Partiality and recursion in interactive theorem provers – an overview
From MaRDI portal
Publication:5741556
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (5)
Partiality and Container Monads ⋮ A two-valued logic for properties of strict functional programs allowing partial functions ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Continuous and monotone machines
Uses Software
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
