Constructing recursion operators in intuitionistic type theory
From MaRDI portal
Publication:1094421
DOI10.1016/S0747-7171(86)80002-5zbMath0631.03045OpenAlexW2005917745WikidataQ57382742 ScholiaQ57382742MaRDI QIDQ1094421
Publication date: 1986
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0747-7171(86)80002-5
Abstract data types; algebraic specification (68Q65) Second- and higher-order arithmetic and fragments (03F35)
Related Items
Termination of rewriting ⋮ Set theory for verification. II: Induction and recursion ⋮ Terminating general recursion ⋮ Formalising Mathematics in Simple Type Theory ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Do-it-yourself type theory ⋮ An intuitionistic version of Ramsey's theorem and its use in program termination ⋮ Program development in constructive type theory ⋮ Building Certified Static Analysers by Modular Construction of Well-founded Lattices ⋮ Partiality and recursion in interactive theorem provers – an overview ⋮ Certifying properties of an efficient functional program for computing Gröbner bases
Uses Software
Cites Work
- Propositions and specifications of programs in Martin-Löf's type theory
- Proving termination of normalization functions for conditional expressions
- Deductive synthesis of the unification algorithm
- Edinburgh LCF. A mechanized logic of computation
- Constructive mathematics and computer programming
- Lessons learned from LCF: A Survey of Natural Deduction Proofs
- An interpretation of Martin-Löf's type theory in a type-free theory of propositions
- A While-rule in Martin-Lof's Theory of Types
- Proving termination with multiset orderings
- On definition trees of ordinal recursive functionals: Reduction of the recursion orders by means of type level raising
- Natural deduction as higher-order resolution
- Functionals defined by transfinite recursion
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Constructing recursion operators in intuitionistic type theory
