Partial and nested recursive function definitions in higher-order logic

DOI10.1007/s10817-009-9157-2zbMath1214.68335OpenAlexW2082393912MaRDI QIDQ972425

Alexander Krauss

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

zbMATH Keywords

partial functionsproof assistantsnested recursion

Mathematics Subject Classification ID

Related Items

ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT, Type Inference for ZFH, A two-valued logic for properties of strict functional programs allowing partial functions, Formalization of the resolution calculus for first-order logic, Deriving Comparators and Show Functions in Isabelle/HOL, Formalising Mathematics in Simple Type Theory, Formalizing network flow algorithms: a refinement approach in Isabelle/HOL, Refinement to imperative HOL, A framework for developing stand-alone certifiers, Partiality and recursion in interactive theorem provers – an overview, Translating Scala Programs to Isabelle/HOL, Termination of Isabelle Functions via Termination of Rewriting, Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism, Proof pearl: A mechanized proof of GHC's mergesort

Uses Software

• ACL2
• Coq
• ML
• Isabelle/HOL
• Isabelle/Isar
• Isar
• Isabelle/ZF
• HOL
• ETPS
• HOL Light
• NQTHM
• LCF
• Nominal Isabelle
• Depth First Search
• Presburger Automata
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Partial functions in a total setting
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Nominal techniques in Isabelle/HOL
• Adapting functional programs to higher order logic
• Verifying the unification algorithm in LCF
• Deductive synthesis of the unification algorithm
• On proving the termination of algorithms by machine
• Termination of nested and mutually recursive algorithms
• Partial functions in ACL2
• Induction proofs with partial functions
• Isabelle/HOL. A proof assistant for higher-order logic
• Termination of term rewriting using dependency pairs
• Formalizing the Logic-Automaton Connection
• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
• Inductive Invariants for Nested Recursion
• Certified Size-Change Termination
• Computation by Prophecy
• Partial Recursive Functions in Higher-Order Logic
• A general formulation of simultaneous inductive-recursive definitions in type theory
• The size-change principle for program termination
• Efficient execution in an automated reasoning environment
• Modelling general recursion in type theory
• Typed Lambda Calculi and Applications
• Types for Proofs and Programs