Typed Applicative Structures and Normalization by Evaluation for System F ω

DOI10.1007/978-3-642-04027-6_6zbMath1257.03037OpenAlexW2132573718MaRDI QIDQ3644739

Andreas Abel

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

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

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

• Coq
• Epigram

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 ω