<html><head></head><body><div style="font-family: Verdana;font-size: 12.0px;"><div>
<div>Hi All,</div>

<div>&nbsp;</div>

<div>I am a Bitcoin enthusiast based in India. I am presently working on creating a decidable programming language codenamed XK for open source free programming on a new blockchain that does not necessarily require a positive cryptocurrency balance or computing fuel reserve unlike Ethereum. Our proposed blockchain will power next generation decentralized autonomous apps and organizations including blockchain banks, hedge funds, prime brokers, stock exchanges, forex dealers, automated software companies/factories and so on. This will empower new entrepreneurs, investors and others those who feel disadvantaged vis-&agrave;-vis big institutional investors and MNCs.</div>

<div>We envision XK to support following four categories of applications and functions primarily:</div>

<ol>
        <li value="NaN">Decentralized trustless financial Contracts (without any need for 3<sup>rd</sup> party custodians like banks and stock exchanges): This list includes equity, forex, commodity and event derivatives e.g. options, functions, swaps, swaptions, cryptostocks, cryptobonds and so on.</li>
        <li value="NaN">Time-aware Self-organizing autonomous systems. This list includes automated trading systems and strategy engines, realtime voice agents like SIRI and realtime activity supervisors and enforcer bots.</li>
        <li value="NaN">Autonomic Dispute Resolution, Blockchain Law/Code Interpretation &amp; Arbitration</li>
        <li value="NaN">Automated software testing, debugging, verification and license distribution as well as tracking.</li>
</ol>

<div>I was thinking of extracting the selected features of Intuitionistic Ancestral Logic with dependent types, Intuitionistic Logic that proves Markov&rsquo;s Principle as well as of Algebraic topology-based self-learning, self-planning and self-executing distributed computing domain Phase Web introduced by Michael Manthey. Phase Web has got connection with both Chu automaton and growing Petrinets (growing in both nodes and connections to reflect complexity, learning, planning etc.).</div>

<div>&nbsp;</div>

<div>How do we adapt your Adga for our purpose? Would it be feasible for us to add desired higher-order capabilities to Agda for our target apps? If yes, what would be the ideal development path and roadmap?</div>

<div>&nbsp;</div>

<div>I look forward to hearing from you.</div>

<div>&nbsp;</div>

<div>Best regards,</div>

<div>Ren Aryan</div>
</div></div></body></html>