Automatizing termination proofs of recursively defined functions
From MaRDI portal
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)- An ordinal measure based procedure for termination of functions
- Inductively defined functions in functional programming languages
- Termination Proofs for Recursive Functions in FoCaLiZe
- AN EXTENSION OF AN AUTOMATED TERMINATION METHOD OF RECURSIVE FUNCTIONS
- Function definition in higher-order logic
- On automating the extraction of programs from proofs using product types
- Decision Procedures for Automating Termination Proofs
- scientific article; zbMATH DE number 1500561 (Why is no real title available?)
- 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
- scientific article; zbMATH DE number 107881 (Why is no real title available?)
- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
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)
