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

DOI10.1007/S10817-021-09615-XOpenAlexW4210693478MaRDI QIDQ2102949FDOQ2102949

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

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

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)

Cites Work

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

Cited In (9)

• Formalizing abstract computability: Turing categories in Coq
• Formal verification of termination criteria for first-order recursive functions
• Algorithmic completeness of imperative programming languages
• A language for easy and efficient modeling of Turing machines
• Title not available (Why is that?)
• Formalization of the undecidability of the halting problem for a functional language
• Computational and attribute models of formal languages
• Mechanised computability theory
• Title not available (Why is that?)

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)