Partial and nested recursive function definitions in higher-order logic (Q972425)

From MaRDI portal

Jump to:navigation, search

scientific article

In more languages

Language	Label	Description	Also known as
English	Partial and nested recursive function definitions in higher-order logic	scientific article

Statements

scholarly article

Partial and nested recursive function definitions in higher-order logic (English)

zbMATH Open document ID

10.1007/s10817-009-9157-2

Alexander Krauss

Journal of Automated Reasoning

publication date

26 May 2010

Mathematics Subject Classification ID

zbMATH DE Number

zbMATH Keywords

proof assistants

partial functions

nested recursion

MaRDI profile type

MaRDI publication profile

full work available at URL

https://doi.org/10.1007/s10817-009-9157-2

Termination of term rewriting using dependency pairs

Types for Proofs and Programs

Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant

Formalizing the Logic-Automaton Connection

Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.

Modelling general recursion in type theory

Typed Lambda Calculi and Applications

Computation by Prophecy

Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL

A general formulation of simultaneous inductive-recursive definitions in type theory

Partial functions in a total setting

Termination of nested and mutually recursive algorithms

Induction proofs with partial functions

Efficient execution in an automated reasoning environment

Partial Recursive Functions in Higher-Order Logic

Certified Size-Change Termination

Inductive Invariants for Nested Recursion

The size-change principle for program termination

Deductive synthesis of the unification algorithm

Partial functions in ACL2

Isabelle/HOL. A proof assistant for higher-order logic

Adapting functional programs to higher order logic

Verifying the unification algorithm in LCF

Nominal techniques in Isabelle/HOL

On proving the termination of algorithms by machine

Sitelinks

Mathematics(1 entry)

mardi Publication:972425

Retrieved from "https://portal.mardi4nfdi.de/w/index.php?title=Item:Q972425&oldid=35171521"