Typed Applicative Structures and Normalization by Evaluation for System F ω
From MaRDI portal
Publication:3644739
DOI10.1007/978-3-642-04027-6_6zbMath1257.03037OpenAlexW2132573718MaRDI QIDQ3644739
Publication date: 12 November 2009
Published in: Computer Science Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-04027-6_6
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (3)
Internal models of system F for decompilation ⋮ Kripke models for classical logic ⋮ Typed Applicative Structures and Normalization by Evaluation for System F ω
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- The lambda calculus. Its syntax and semantics. Rev. ed.
- An algorithm for type-checking dependent types
- Intuitionistic model constructions and normalization proofs
- A compiled implementation of strong reduction
- Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums
- Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
- Typed Applicative Structures and Normalization by Evaluation for System F ω
- Categorical semantics for higher order polymorphic lambda calculus
- A general formulation of simultaneous inductive-recursive definitions in type theory
- Weak βη-Normalization and Normalization by Evaluation for System F
This page was built for publication: Typed Applicative Structures and Normalization by Evaluation for System F ω
