Strong Normalization of Moggis's Computational Metalanguage
From MaRDI portal
- A formalization of strong normalization for simply-typed lambda-calculus and System F
- A framework for defining logics
- A unification algorithm for typed \(\bar\lambda\)-calculus
- Alpha-structural recursion and induction
- Barendregt’s Variable Convention in Rule Inductions
- Computational types from a logical perspective
- Domain-free pure type systems
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Isabelle. A generic theorem prover
- Nominal Inversion Principles
- Normalization for the simply-typed lambda-calculus in Twelf
- Program extraction from normalization proofs
- Some lambda calculus and type theory formalized
- Sur les correspondances multivoques des ensembles.
- The foundation of a generic theorem prover
- Theorem Proving in Higher Order Logics
- Typed Lambda Calculi and Applications
This page was built for software: Strong Normalization of Moggis's Computational Metalanguage
