Weak normalization implies strong normalization in a class of non-dependent pure type systems
From MaRDI portal
Publication:5958619
DOI10.1016/S0304-3975(01)00012-3zbMath0983.68029MaRDI QIDQ5958619
Morten Heine B. Sørensen, John Hatcliff, Gilles Barthe
Publication date: 3 March 2002
Published in: Theoretical Computer Science (Search for Journal in Brave)
68N18: Functional programming and lambda calculus
Related Items
Unnamed Item, Monadic translation of classical sequent calculus, An induction principle for pure type systems, Conservation and uniform normalization in lambda calculi with erasing reductions, Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
Uses Software
Cites Work
- The lambda calculus. Its syntax and semantics. Rev. ed.
- CPS translations and applications: The cube and beyond
- On the adequacy of representing higher order intuitionistic logic as a pure type system
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Strong normalization from weak normalization in typed \(\lambda\)-calculi
- A-translation and looping combinators in pure type systems
- Some Properties of Conversion
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item