scientific article; zbMATH DE number 512769
From MaRDI portal
Publication:4281462
zbMath0797.68095MaRDI QIDQ4281462
Publication date: 10 March 1994
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
calculus of constructionsinductive typesstrong normalizationsaturated setscandidates of reducibilitycomputer aided formal reasoning
Related Items
Coq formalization of the higher-order recursive path ordering ⋮ Reverse mathematical bounds for the termination theorem ⋮ A formalization of the Knuth-Bendix(-Huet) critical pair theorem ⋮ Formalization of a λ-calculus with explicit substitutions in Coq ⋮ Proving strong normalization of CC by modifying realizability semantics ⋮ Closure under alpha-conversion ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ A solution to the PoplMark challenge based on de Bruijn indices ⋮ An intuitionistic version of Ramsey's theorem and its use in program termination ⋮ A PVS Theory for Term Rewriting Systems ⋮ Programming Inductive Proofs ⋮ Mechanizing proofs with logical relations – Kripke-style ⋮ Mechanized metatheory revisited ⋮ A Third-Order Representation of the λμ-Calculus ⋮ Normalization for the Simply-Typed Lambda-Calculus in Twelf
Uses Software
This page was built for publication:
