[Agda] How can I implement naive sized lambdas?
Philip Wadler
wadler at inf.ed.ac.uk
Sun Apr 5 15:24:55 CEST 2020
>
> That said, is there some "well-scoped syntaxes 101" resource that I could
> read?
Programming Language Foundations in Agda contains a beginners guide to
lambda calculus in both extrinsic (named variables, separate type rules)
and intrinsic (deBruijn, inherently scoped and typed) forms. Go well, -- P
plfa.inf.ed.ac.uk
plfa.inf.ed.ac.uk/Lambda/
plfa.inf.ed.ac.uk/Properties/
plfa.inf.ed.ac.uk/DeBruijn/
. \ 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/20200405/0ec36c71/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200405/0ec36c71/attachment.ksh>
More information about the Agda
mailing list