Intuitionistic model constructions and normalization proofs
From MaRDI portal
Recommendations
Cited in
(23)- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- A logical framework combining model and proof theory
- Categorical reconstruction of a reduction free normalization proof
- Term rewriting for normalization by evaluation.
- Representing model theory in a type-theoretical logical framework
- Semantic analysis of normalisation by evaluation for typed lambda calculus
- The simple type theory of normalisation by evaluation
- A new model construction by making a detour via intuitionistic theories. II: Interpretability lower bound of Feferman's explicit mathematics \(T_0\)
- Internal type theory
- Intuitionistic validity in \(T\)-normal Kripke structures
- A general formulation of simultaneous inductive-recursive definitions in type theory
- Categorical structure in coherent theory of arithmetic
- A context-based approach to proving termination of evaluation
- Normalization by Evaluation for Typed Weak lambda-Reduction
- Models of intuitionistic TT and NF
- Big-step normalisation
- Normalization by evaluation for modal dependent type theory
- Denotational aspects of untyped normalization by evaluation
- On Normalization by Evaluation for Object Calculi
- Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids
- Typed Applicative Structures and Normalization by Evaluation for System F ω
- Program extraction from normalization proofs
- Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation
This page was built for publication: Intuitionistic model constructions and normalization proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2785696)
