Loading...
Please wait, while we are loading the content...
Similar Documents
Deriving the full-reducing krivine machine from the small-step operational semantics of normal order (2013).
| Content Provider | CiteSeerX |
|---|---|
| Author | García-Pérez, Álvaro Nogueira, Pablo Moreno-Navarro, Juan José |
| Description | DRAFT SUBMITTED TO ICFP 2013 |
| Abstract | Pierre Crégut’s full-reducing Krivine machine KN is a push/enter, environment-based abstract machine that normalises closed pure lambda calculus terms. Normal order is the standard, complete, full-reducing reduction strategy of the pure lambda calculus. In this paper we derive the machine by means of program-transformation from the small-step operational semantics of normal order in a calculus of closures. Actually, the machine we obtain is a slightly optimised version that can work with open terms and is therefore suitable for use in implementations of proof assistants. |
| File Format | |
| Publisher Date | 2013-01-01 |
| Access Restriction | Open |
| Subject Keyword | Normal Order Small-step Operational Semantics Full-reducing Krivine Machine Full-reducing Reduction Strategy Push Enter Pierre Cr Gut Pure Lambda Calculus Open Term Closed Pure Lambda Calculus Term Full-reducing Krivine Machine Kn Environment-based Abstract Machine Proof Assistant |
| Content Type | Text |
| Resource Type | Article |
