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

DOI10.1007/s10817-021-09615-xOpenAlexW4210693478MaRDI QIDQ2102949

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)

Related Items (1)

Formal verification of termination criteria for first-order recursive functions

Uses Software

• Coq
• PVS

Cites Work

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

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