Publication:4281462
From MaRDI portal
zbMath0797.68095MaRDI QIDQ4281462
Publication date: 10 March 1994
calculus of constructions; inductive types; strong normalization; saturated sets; candidates of reducibility; computer aided formal reasoning
Related Items
Mechanizing proofs with logical relations – Kripke-style, POPLMark reloaded: Mechanizing proofs by logical relations, A PVS Theory for Term Rewriting Systems, Reverse mathematical bounds for the termination theorem, An intuitionistic version of Ramsey's theorem and its use in program termination, A formalization of the Knuth-Bendix(-Huet) critical pair theorem, Coq formalization of the higher-order recursive path ordering, A solution to the PoplMark challenge based on de Bruijn indices, Mechanized metatheory revisited, A Third-Order Representation of the λμ-Calculus, Normalization for the Simply-Typed Lambda-Calculus in Twelf, Programming Inductive Proofs
Uses Software