Loading...
Please wait, while we are loading the content...
Similar Documents
A proof of strong normalisation of the typed atomic lambda-calculus.
| Content Provider | CiteSeerX |
|---|---|
| Author | Gundersen, Tom Heijltjes, Willem Parigot, Michel |
| Abstract | Abstract. The atomic lambda-calculus is a typed lambda-calculus with explicit sharing, which originates in a Curry-Howard interpretation of a deep-inference system for intuitionistic logic. It has been shown that it allows fully lazy sharing to be reproduced in a typed setting. In this paper we prove strong normalization of the typed atomic lambda-calculus using Tait’s reducibility method. 1 |
| File Format | |
| Access Restriction | Open |
| Subject Keyword | Typed Atomic Strong Normalisation Explicit Sharing Strong Normalization Intuitionistic Logic Curry-howard Interpretation Typed Setting Atomic Lambda-calculus Tait Reducibility Method Typed Lambda-calculus Deep-inference System |
| Content Type | Text |
| Resource Type | Article |
