Partiality and recursion in interactive theorem provers – an overview

DOI10.1017/S0960129514000115zbMath1361.68186OpenAlexW2023353691MaRDI QIDQ5741556

Ana Bove, Alexander Krauss, Matthieu Sozeau

Publication date: 28 July 2016

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129514000115

Mathematics Subject Classification ID

Related Items (6)

Partiality and Container Monads ⋮ A two-valued logic for properties of strict functional programs allowing partial functions ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Formal definitions and proofs for partial (co)recursive functions ⋮ Continuous and monotone machines

Uses Software

• Unnamed Item
• Unnamed Item
• Haskell
• Agda

Cites Work

• 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.
• Notions of computation and monads
• A logic covering undefinedness in program proofs
• Partial and nested recursive function definitions in higher-order logic
• Adapting functional programs to higher order logic
• Constructing recursion operators in intuitionistic type theory
• The calculus of constructions
• Terminating general recursion
• A type-theoretical alternative to ISWIM, CUCH, OWHY
• A simple type theory with partial functions and subtypes
• Termination of nested and mutually recursive algorithms
• Partial functions in ACL2
• Induction proofs with partial functions
• The foundation of a generic theorem prover
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs
• First-order unification by structural recursion
• A Purely Definitional Universal Domain
• Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
• Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
• Type-Based Termination with Sized Products
• Code Generation via Higher-Order Rewrite Systems
• Inductive Invariants for Nested Recursion
• Certified Size-Change Termination
• Computation by Prophecy
• The Theoretical Aspects of the Optimal Fixedpoint
• HOLCF = HOL + LCF
• Type-based termination of recursive definitions
• A general formulation of simultaneous inductive-recursive definitions in type theory
• The view from the left
• A Tutorial on Type-Based Termination
• CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
• Modelling general recursion in type theory
• Eliminating Dependent Pattern Matching

This page was built for publication: Partiality and recursion in interactive theorem provers – an overview