Partiality and recursion in interactive theorem provers -- an overview
From MaRDI portal
Recommendations
Cites work
- A general formulation of simultaneous inductive-recursive definitions in type theory
- A logic covering undefinedness in program proofs
- A Purely Definitional Universal Domain
- A simple type theory with partial functions and subtypes
- A Tutorial on Type-Based Termination
- A type-theoretical alternative to ISWIM, CUCH, OWHY
- Adapting functional programs to higher order logic
- Certified Size-Change Termination
- CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
- Code generation via higher-order rewrite systems
- Combining interactive and automatic reasoning in first order theories of functional programs
- Computation by Prophecy
- Constructing recursion operators in intuitionistic type theory
- Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
- Eliminating Dependent Pattern Matching
- Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
- First-order unification by structural recursion
- HOLCF = HOL + LCF
- scientific article; zbMATH DE number 46957 (Why is no real title available?)
- scientific article; zbMATH DE number 50149 (Why is no real title available?)
- scientific article; zbMATH DE number 1952947 (Why is no real title available?)
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- Induction proofs with partial functions
- Inductive invariants for nested recursion
- 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
- Notions of computation and monads
- Partial and nested recursive function definitions in higher-order logic
- Partial functions in a total setting
- Partial functions in ACL2
- Terminating general recursion
- Termination of nested and mutually recursive algorithms
- The calculus of constructions
- The foundation of a generic theorem prover
- The Theoretical Aspects of the Optimal Fixedpoint
- The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
- The view from the left
- Type-based termination of recursive definitions
- Type-Based Termination with Sized Products
Cited in
(13)- Interactive theorem proving. Preface of the special issue
- Partiality, state and dependent types
- A Purely Definitional Universal Domain
- A two-valued logic for properties of strict functional programs allowing partial functions
- scientific article; zbMATH DE number 4074542 (Why is no real title available?)
- Partiality and Container Monads
- Continuous and monotone machines
- Pattern minimization problems over recursive data types
- scientific article; zbMATH DE number 7649962 (Why is no real title available?)
- Formalized proof systems for propositional logic
- A step-indexing approach to partial functions
- Formal definitions and proofs for partial (co)recursive functions
- Program optimisations via hylomorphisms for extraction of executable code
This page was built for publication: Partiality and recursion in interactive theorem provers -- an overview
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5741556)
