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)
Related Items (5)
Unnamed Item ⋮ Monadic translation of classical sequent calculus ⋮ An induction principle for pure type systems ⋮ Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions ⋮ Conservation and uniform normalization in lambda calculi with erasing reductions
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- 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
This page was built for publication: Weak normalization implies strong normalization in a class of non-dependent pure type systems