Formalization of the computational theory of a Turing complete functional language model

DOI10.1007/S10817-021-09615-XMaRDI QIDQ2102949zbMATH OpenOpenAlexFDO

Authors Thiago Mendonça Ferreira Ramos, Ariane Alves Almeida, Mauricio Ayala-Rincón

Publication date 12 December 2022

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-021-09615-x

zbMATH Keywords

theorem provingcomputability theoryRice's theoremPVSHalting problemautomating terminationfunctional programming models

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Mechanised computability theory
• Formalization of the undecidability of the halting problem for a functional language
• scientific article; zbMATH DE number 3938596
• Formalizing abstract computability: Turing categories in Coq
• Mechanising Turing machines and computability theory in Isabelle/HOL

Cites work

• scientific article; zbMATH DE number 5595162 (Why is no real title available?)
• scientific article; zbMATH DE number 1517989 (Why is no real title available?)
• scientific article; zbMATH DE number 2085172 (Why is no real title available?)
• scientific article; zbMATH DE number 3057871 (Why is no real title available?)
• scientific article; zbMATH DE number 7649961 (Why is no real title available?)
• scientific article; zbMATH DE number 7699444 (Why is no real title available?)
• A Mechanical Proof of the Unsolvability of the Halting Problem
• Formalization of the undecidability of the halting problem for a functional language
• Hilbert's Tenth Problem in Coq
• Mechanised computability theory
• Recursive unsolvability of a problem of Thue
• Termination Analysis with Calling Context Graphs
• Termination by absence of infinite chains of dependency pairs
• Termination of term rewriting using dependency pairs
• The size-change principle for program termination
• The undecidability of the second-order unification problem
• Trakhtenbrot’s Theorem in Coq
• Typing total recursive functions in Coq
• Verification of PCP-related computational reductions in Coq
• Weak call-by-value lambda calculus as a model of computation in Coq

Cited in

(10)

• Formalization of the undecidability of the halting problem for a functional language
• Formal verification of termination criteria for first-order recursive functions
• A language for easy and efficient modeling of Turing machines
• Mechanised computability theory
• Algorithmic completeness of imperative programming languages
• Computational and attribute models of formal languages
• scientific article; zbMATH DE number 2085172 (Why is no real title available?)
• scientific article; zbMATH DE number 3938596 (Why is no real title available?)
• A mechanisation of computability theory in HOL
• Formalizing abstract computability: Turing categories in Coq

Describes a project that uses

Uses Software

• Coq
• PVS

This page was built for publication: Formalization of the computational theory of a Turing complete functional language model

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