Partial and nested recursive function definitions in higher-order logic
From MaRDI portal
Publication:972425
Recommendations
- Partial Recursive Functions in Higher-Order Logic
- Partiality and recursion in higher-order logic
- scientific article; zbMATH DE number 4210120
- scientific article; zbMATH DE number 1163990
- Logical Approaches to Computational Barriers
- scientific article; zbMATH DE number 1863381
- scientific article; zbMATH DE number 4043253
- On modal logics of partial recursive functions
- Formalization of properties of recursively defined functions
- scientific article; zbMATH DE number 1670754
Cites work
- scientific article; zbMATH DE number 1670762 (Why is no real title available?)
- scientific article; zbMATH DE number 3702108 (Why is no real title available?)
- scientific article; zbMATH DE number 193479 (Why is no real title available?)
- scientific article; zbMATH DE number 1301860 (Why is no real title available?)
- scientific article; zbMATH DE number 2003149 (Why is no real title available?)
- scientific article; zbMATH DE number 3999882 (Why is no real title available?)
- scientific article; zbMATH DE number 2085164 (Why is no real title available?)
- scientific article; zbMATH DE number 1863381 (Why is no real title available?)
- scientific article; zbMATH DE number 1424012 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- A general formulation of simultaneous inductive-recursive definitions in type theory
- Adapting functional programs to higher order logic
- Certified Size-Change Termination
- Computation by Prophecy
- Deductive synthesis of the unification algorithm
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
- Efficient execution in an automated reasoning environment
- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
- Formalizing the Logic-Automaton Connection
- Induction proofs with partial functions
- Inductive invariants for nested recursion
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Isabelle/HOL. A proof assistant for higher-order logic
- Modelling general recursion in type theory
- Nominal techniques in Isabelle/HOL
- On proving the termination of algorithms by machine
- Partial Recursive Functions in Higher-Order Logic
- Partial functions in ACL2
- Partial functions in a total setting
- Termination of nested and mutually recursive algorithms
- Termination of term rewriting using dependency pairs
- The size-change principle for program termination
- Typed Lambda Calculi and Applications
- Types for Proofs and Programs
- Verifying the unification algorithm in LCF
Cited in
(23)- Translating Scala programs to Isabelle/HOL. System description
- scientific article; zbMATH DE number 2085164 (Why is no real title available?)
- Partial Recursive Functions in Higher-Order Logic
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
- scientific article; zbMATH DE number 2185679 (Why is no real title available?)
- Type inference for ZFH
- Formalising Mathematics in Simple Type Theory
- A two-valued logic for properties of strict functional programs allowing partial functions
- Proof pearl: A mechanized proof of GHC's mergesort
- ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT
- Inductive invariants for nested recursion
- Formalization of the resolution calculus for first-order logic
- Verified efficient enumeration of plane graphs modulo isomorphism
- scientific article; zbMATH DE number 1670762 (Why is no real title available?)
- Partiality and recursion in interactive theorem provers -- an overview
- Function definition in higher-order logic
- Refinement to imperative HOL
- A framework for developing stand-alone certifiers
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Deriving comparators and show functions in Isabelle/HOL
- Termination of Isabelle functions via termination of rewriting
- Partiality and recursion in higher-order logic
- A step-indexing approach to partial functions
Describes a project that uses
Uses Software
This page was built for publication: Partial and nested recursive function definitions in higher-order logic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q972425)
