<div dir="ltr">What is your favourite way to define lambda calculus in Agda? I am looking for solutions both operational and denotational, and both typed and untyped.<div><br></div><div>My favourite denotational untyped solution so far is due to Nils Anders Danielsson:</div><div><br></div><div>  <a href="http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html">http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html</a></div><div><br></div><div>It defines values as closures, a syntactic approach. What would be even better is to define values semantically:</div><div><br></div><div>  data value where</div><div>     fun : (value -> Delay value) -> value</div><div><br></div><div>But this does not work because value appears in a negative position. Is there a way to model a denotational description of values in Agda, perhaps by mimicking one of the constructions of domain theory?</div><div><br></div><div>Thank you for your help! Cheers, -- P</div><div><br></div><div><br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr">.   \ Philip Wadler, Professor of Theoretical Computer Science,<br>.   /\ School of Informatics, University of Edinburgh<br></div><div>.  /  \ and Senior Research Fellow, IOHK<br></div><div dir="ltr">. <span><a href="http://homepages.inf.ed.ac.uk/wadler/" target="_blank">http://homepages.inf.ed.ac.uk/wadler/</a></span></div></div></div></div></div>
</div></div>