Normalization by Evaluation for Typed Weak lambda-Reduction
From MaRDI portal
Publication:5091147
DOI10.4230/LIPIcs.TYPES.2018.6OpenAlexW3194008643MaRDI QIDQ5091147
Publication date: 21 July 2022
Full work available at URL: http://drops.dagstuhl.de/opus/volltexte/2019/11410/pdf/LIPIcs-TYPES-2018-6.pdf/
Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation
- The lambda calculus. Its syntax and semantics. Rev. ed.
- A minimalist two-level foundation for constructive mathematics
- Combinatory weak reduction in lambda calculus
- Constructivism in mathematics. An introduction. Volume I
- Call-by-need, neededness and all that
- Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice
- The locally nameless representation
- Intuitionistic model constructions and normalization proofs
- Practical Foundations for Programming Languages
- Reasoning About Call-by-need by Means of Types
- Type theory in type theory using quotient inductive types
- Pure Type System conversion is always typable
- A Brief Overview of Agda – A Functional Language with Dependent Types
- A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
- Big-step normalisation
- Confluence properties of weak and strong calculi of explicit substitutions
- Operational aspects of untyped Normalisation by Evaluation
- Explicit substitutions
- Normalization by Evaluation for Martin-Löf Type Theory with One Universe
- Intensional interpretations of functionals of finite type I
- A generalization of the Takeuti–Gandy interpretation
This page was built for publication: Normalization by Evaluation for Typed Weak lambda-Reduction
