Typing total recursive functions in Coq

DOI10.1007/978-3-319-66107-0_24zbMath1484.68313OpenAlexW2746877179MaRDI QIDQ1687755

Dominique Larchey-Wendling

Publication date: 4 January 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-66107-0_24

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Recursive functions and relations, subrecursive hierarchies (03D20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (5)

Typing total recursive functions in Coq ⋮ Unnamed Item ⋮ Hilbert's Tenth Problem in Coq ⋮ Call-by-value lambda calculus as a model of computation in Coq ⋮ Formalization of the computational theory of a Turing complete functional language model

Uses Software

• Coq

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Typing total recursive functions in Coq
• Mechanised Computability Theory
• Mechanising Turing Machines and Computability Theory in Isabelle/HOL
• Modelling general recursion in type theory

This page was built for publication: Typing total recursive functions in Coq