Partial and nested recursive function definitions in higher-order logic
type: Item
instance of: scholarly article
title: Partial and nested recursive function definitions in higher-order logic
zbMATH Open document ID: 1214.68335
author: Alexander Krauss
published in: Journal of Automated Reasoning
publication date: 2010-05-26T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 5711941
zbMATH Keywords: proof assistants
zbMATH Keywords: partial functions
zbMATH Keywords: nested recursion
describes a project that uses: ML
describes a project that uses: ETPS
describes a project that uses: HOL Light
describes a project that uses: LCF
describes a project that uses: Coq
describes a project that uses: Isabelle/HOL
describes a project that uses: Isar
describes a project that uses: Isabelle/ZF
describes a project that uses: Depth First Search
describes a project that uses: ACL2
describes a project that uses: Isabelle/Isar
describes a project that uses: HOL
describes a project that uses: NQTHM
describes a project that uses: Nominal Isabelle
describes a project that uses: Presburger Automata
describes a project that uses: Archive Formal Proofs
MaRDI profile type: Publication
full work available at URL: s10817-009-9157-2
OpenAlex ID: W2082393912
cites work: Q4726218
cites work: Termination of term rewriting using dependency pairs
cites work: Types for Proofs and Programs
cites work: Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
cites work: Q4736387
cites work: Formalizing the Logic-Automaton Connection
cites work: Q4945200
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Q4435459
cites work: Q4790656
cites work: Modelling general recursion in type theory
cites work: Typed Lambda Calculi and Applications
cites work: Computation by Prophecy
cites work: Q3894958
cites work: Q4040283
cites work: Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
cites work: A general formulation of simultaneous inductive-recursive definitions in type theory
cites work: Partial functions in a total setting
cites work: Termination of nested and mutually recursive algorithms
cites work: Induction proofs with partial functions
cites work: Q5287513
cites work: Efficient execution in an automated reasoning environment
cites work: Partial Recursive Functions in Higher-Order Logic
cites work: Certified Size-Change Termination
cites work: Inductive Invariants for Nested Recursion
cites work: The size-change principle for program termination
cites work: Deductive synthesis of the unification algorithm
cites work: Partial functions in ACL2
cites work: Q4247084
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Adapting functional programs to higher order logic
cites work: Verifying the unification algorithm in LCF
cites work: Q2754066
cites work: Nominal techniques in Isabelle/HOL
cites work: On proving the termination of algorithms by machine
DOI: 10.1007/S10817-009-9157-2
Recommended article: Partial Recursive Functions in Higher-Order Logic
Recommended article: Partiality and Recursion in Higher-Order Logic
Recommended article: Q3358718
Recommended article: Q4395617
Recommended article: Logical Approaches to Computational Barriers
Recommended article: Q4790656
Recommended article: Q3780444
Recommended article: On modal logics of partial recursive functions
Recommended article: Formalization of properties of recursively defined functions
Recommended article: Q2754055
description: scientific article; zbMATH DE number 5711941