Partial and nested recursive function definitions in higher-order logic
From MaRDI portal
Publication:972425
DOI10.1007/S10817-009-9157-2zbMATH Open1214.68335OpenAlexW2082393912MaRDI QIDQ972425FDOQ972425
Publication date: 26 May 2010
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-009-9157-2
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Nominal techniques in Isabelle/HOL
- Formalizing the Logic-Automaton Connection
- Isabelle/HOL. A proof assistant for higher-order logic
- Termination of term rewriting using dependency pairs
- The size-change principle for program termination
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Partial functions in ACL2
- Types for Proofs and Programs
- Induction proofs with partial functions
- Partial Recursive Functions in Higher-Order Logic
- Partial functions in a total setting
- On proving the termination of algorithms by machine
- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
- Certified Size-Change Termination
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
- A general formulation of simultaneous inductive-recursive definitions in type theory
- Computation by Prophecy
- Modelling general recursion in type theory
- Deductive synthesis of the unification algorithm
- Adapting functional programs to higher order logic
- Verifying the unification algorithm in LCF
- Termination of nested and mutually recursive algorithms
- Inductive Invariants for Nested Recursion
- Efficient execution in an automated reasoning environment
- Typed Lambda Calculi and Applications
Cited In (15)
- A framework for developing stand-alone certifiers
- Refinement to imperative HOL
- Termination of Isabelle Functions via Termination of Rewriting
- Proof pearl: A mechanized proof of GHC's mergesort
- Formalization of the resolution calculus for first-order logic
- A step-indexing approach to partial functions
- Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism
- Formalising Mathematics in Simple Type Theory
- Partiality and recursion in interactive theorem provers – an overview
- Deriving Comparators and Show Functions in Isabelle/HOL
- Translating Scala Programs to Isabelle/HOL
- ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT
- A two-valued logic for properties of strict functional programs allowing partial functions
- Type Inference for ZFH
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
Uses Software
Recommendations
- Title not available (Why is that?) 👍 👎
- Title not available (Why is that?) 👍 👎
- Title not available (Why is that?) 👍 👎
- Title not available (Why is that?) 👍 👎
- Title not available (Why is that?) 👍 👎
- Partial Recursive Functions in Higher-Order Logic 👍 👎
- Partiality and Recursion in Higher-Order Logic 👍 👎
- On modal logics of partial recursive functions 👍 👎
- Formalization of properties of recursively defined functions 👍 👎
- Logical Approaches to Computational Barriers 👍 👎
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)
