Automatizing termination proofs of recursively defined functions
From MaRDI portal
Publication:1346629
DOI10.1016/0304-3975(94)00021-2zbMATH Open0829.68031OpenAlexW1990295079MaRDI QIDQ1346629FDOQ1346629
Authors: Pascal Manoury, M. Simonot 
Publication date: 6 April 1995
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(94)00021-2
Recommendations
- scientific article; zbMATH DE number 107881
- scientific article; zbMATH DE number 1487841
- AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS
- Termination Proofs for Recursive Functions in FoCaLiZe
- scientific article; zbMATH DE number 108494
- Automatic proofs of termination with elementary interpretations
- Automatic Termination Verification for Higher-Order Functional Programs
- Automata-Based Termination Proofs
- Automata-based termination proofs
Cites Work
Cited In (16)
- Inductively defined functions in functional programming languages
- Function definition in higher-order logic
- AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS
- Termination Proofs for Recursive Functions in FoCaLiZe
- On automating the extraction of programs from proofs using product types
- Decision Procedures for Automating Termination Proofs
- Title not available (Why is that?)
- A user's friendly syntax to define recursive functions as typed λ-terms
- Automatic Termination Verification for Higher-Order Functional Programs
- Automating Side Conditions in Formalized Partial Functions
- Automating inversion of inductive predicates in Coq
- Termination of Isabelle functions via termination of rewriting
- Automatically Introducing Tail Recursion in CakeML
- Title not available (Why is that?)
- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
- An ordinal measure based procedure for termination of functions
This page was built for publication: Automatizing termination proofs of recursively defined functions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1346629)
