Typing total recursive functions in Coq

DOI10.1007/978-3-319-66107-0_24MaRDI QIDQ1687755zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• General Recursion via Coinductive Types
• Synthesis of ML programs in the system Coq
• Simple general recursion in type theory
• Computation by Prophecy
• scientific article; zbMATH DE number 1670732

Cites work

• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 194103 (Why is no real title available?)
• scientific article; zbMATH DE number 482822 (Why is no real title available?)
• scientific article; zbMATH DE number 1088050 (Why is no real title available?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Mechanised computability theory
• Mechanising Turing machines and computability theory in Isabelle/HOL
• Modelling general recursion in type theory
• Typing total recursive functions in Coq

Cited in

(11)

• Call-by-value lambda calculus as a model of computation in Coq
• Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages
• scientific article; zbMATH DE number 7566048 (Why is no real title available?)
• General Recursion via Coinductive Types
• Computation by Prophecy
• Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant
• A user's friendly syntax to define recursive functions as typed λ-terms
• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• Hilbert's Tenth Problem in Coq
• Typing total recursive functions in Coq
• Formalization of the computational theory of a Turing complete functional language model

Describes a project that uses

Uses Software

• Coq

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1687755)