From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine
This paper presents the derivation of an executable Krivine abstract machine from a small step interpreter for the simply typed lambda calculus in the dependently typed programming language Agda.
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2012-02-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1202.2924v1 |
| _version_ | 1818361809682300928 |
|---|---|
| author | Wouter Swierstra |
| author_facet | Wouter Swierstra |
| author_sort | Wouter Swierstra |
| collection | DOAJ |
| description | This paper presents the derivation of an executable Krivine abstract machine from a small step interpreter for the simply typed lambda calculus in the dependently typed programming language Agda. |
| first_indexed | 2024-12-13T21:22:35Z |
| format | Article |
| id | doaj.art-23faed0e69834ccd9719df3db67c010f |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-13T21:22:35Z |
| publishDate | 2012-02-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-23faed0e69834ccd9719df3db67c010f2022-12-21T23:31:03ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802012-02-0176Proc. MSFP 201216317710.4204/EPTCS.76.10From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machineWouter SwierstraThis paper presents the derivation of an executable Krivine abstract machine from a small step interpreter for the simply typed lambda calculus in the dependently typed programming language Agda.http://arxiv.org/pdf/1202.2924v1 |
| spellingShingle | Wouter Swierstra From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine Electronic Proceedings in Theoretical Computer Science |
| title | From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine |
| title_full | From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine |
| title_fullStr | From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine |
| title_full_unstemmed | From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine |
| title_short | From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine |
| title_sort | from mathematics to abstract machine a formal derivation of an executable krivine machine |
| url | http://arxiv.org/pdf/1202.2924v1 |
| work_keys_str_mv | AT wouterswierstra frommathematicstoabstractmachineaformalderivationofanexecutablekrivinemachine |