Big-step normalisation
From MaRDI portal
Recommendations
- A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
- Foundations of Software Science and Computation Structures
- Interpolation for Brill-Noether space curves
- scientific article; zbMATH DE number 1342288
- The simple type theory of normalisation by evaluation
Cites work
- scientific article; zbMATH DE number 50149 (Why is no real title available?)
- A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions
- Extensional Rewriting with Sums
- Intensional interpretations of functionals of finite type I
- Intuitionistic model constructions and normalization proofs
- Normalization without reducibility
- The view from the left
- The virtues of eta-expansion
Cited in
(13)- The exp-log normal form of types: decomposing extensional equality and representing terms compactly
- scientific article; zbMATH DE number 2185727 (Why is no real title available?)
- Towards a cubical type theory without an interval
- Decidability for non-standard conversions in typed lambda-calculi
- Pure type systems with explicit substitutions
- Normalization by Evaluation for Typed Weak lambda-Reduction
- Normalization flow
- Structural recursion with locally scoped names
- Indexed containers
- Implementing a normalizer using sized heterogeneous types
- Big step normalisation for type theory
- scientific article; zbMATH DE number 6792365 (Why is no real title available?)
- Type theory should eat itself
This page was built for publication: Big-step normalisation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3638919)
