[Agda] Operational and Denotational, Typed and Untyped Lambda Calculus

[Philip Wadler]

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.

My favourite denotational untyped solution so far is due to Nils Anders
Danielsson:


http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html

It defines values as closures, a syntactic approach. What would be even
better is to define values semantically:

  data value where
     fun : (value -> Delay value) -> value

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?

Thank you for your help! Cheers, -- P


.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180329/04e94356/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180329/04e94356/attachment.ksh>