Partiality and recursion in interactive theorem provers – an overview (Q5741556): Difference between revisions

@@ Property / describes a project that uses @@
+Agda
@@ Property / describes a project that uses: Agda / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Isabelle/HOL
@@ Property / describes a project that uses: Isabelle/HOL / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs
+Normal rank
@@ Property / cites work @@
+Adapting functional programs to higher order logic
+Normal rank
@@ Property / cites work @@
+Computation by Prophecy
@@ Property / cites work: Computation by Prophecy / rank @@
+Normal rank
@@ Property / cites work @@
+Modelling general recursion in type theory
@@ Property / cites work: Modelling general recursion in type theory / rank @@
+Normal rank
@@ Property / cites work @@
+Q3999860
@@ Property / cites work: Q3999860 / rank @@
+Normal rank
@@ Property / cites work @@
+Terminating general recursion
@@ Property / cites work: Terminating general recursion / rank @@
+Normal rank
@@ Property / cites work @@
+HOLCF = HOL + LCF
@@ Property / cites work: HOLCF = HOL + LCF / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Notions of computation and monads
@@ Property / cites work: Notions of computation and monads / rank @@
+Normal rank
@@ Property / cites work @@
+The view from the left
@@ Property / cites work: The view from the left / rank @@
+Normal rank
@@ Property / cites work @@
+A Tutorial on Type-Based Termination
@@ Property / cites work: A Tutorial on Type-Based Termination / rank @@
+Normal rank
@@ Property / cites work @@
+First-order unification by structural recursion
@@ Property / cites work: First-order unification by structural recursion / rank @@
+Normal rank
@@ Property / cites work @@
+Partial functions in ACL2
@@ Property / cites work: Partial functions in ACL2 / rank @@
+Normal rank
@@ Property / cites work @@
+The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
+Normal rank
@@ Property / cites work @@
+Type-Based Termination with Sized Products
@@ Property / cites work: Type-Based Termination with Sized Products / rank @@
+Normal rank
@@ Property / cites work @@
+CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
+Normal rank
@@ Property / cites work @@
+Type-based termination of recursive definitions
@@ Property / cites work: Type-based termination of recursive definitions / rank @@
+Normal rank
@@ Property / cites work @@
+Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant
+Normal rank
@@ Property / cites work @@
+A logic covering undefinedness in program proofs
@@ Property / cites work: A logic covering undefinedness in program proofs / rank @@
+Normal rank
@@ Property / cites work @@
+The Theoretical Aspects of the Optimal Fixedpoint
@@ Property / cites work: The Theoretical Aspects of the Optimal Fixedpoint / rank @@
+Normal rank
@@ Property / cites work @@
+Inductive Invariants for Nested Recursion
@@ Property / cites work: Inductive Invariants for Nested Recursion / rank @@
+Normal rank
@@ Property / cites work @@
+Partial and nested recursive function definitions in higher-order logic
+Normal rank
@@ Property / cites work @@
+Certified Size-Change Termination
@@ Property / cites work: Certified Size-Change Termination / rank @@
+Normal rank
@@ Property / cites work @@
+Q3997074
@@ Property / cites work: Q3997074 / rank @@
+Normal rank
@@ Property / cites work @@
+A type-theoretical alternative to ISWIM, CUCH, OWHY
+Normal rank
@@ Property / cites work @@
+Q4414308
@@ Property / cites work: Q4414308 / rank @@
+Normal rank
@@ Property / cites work @@
+The foundation of a generic theorem prover
@@ Property / cites work: The foundation of a generic theorem prover / rank @@
+Normal rank
@@ Property / cites work @@
+Constructing recursion operators in intuitionistic type theory
+Normal rank
@@ Property / cites work @@
+A Purely Definitional Universal Domain
@@ Property / cites work: A Purely Definitional Universal Domain / rank @@
+Normal rank
@@ Property / cites work @@
+Code Generation via Higher-Order Rewrite Systems
@@ Property / cites work: Code Generation via Higher-Order Rewrite Systems / rank @@
+Normal rank
@@ Property / cites work @@
+Q5287513
@@ Property / cites work: Q5287513 / rank @@
+Normal rank
@@ Property / cites work @@
+Eliminating Dependent Pattern Matching
@@ Property / cites work: Eliminating Dependent Pattern Matching / rank @@
+Normal rank
@@ Property / cites work @@
+Induction proofs with partial functions
@@ Property / cites work: Induction proofs with partial functions / rank @@
+Normal rank
@@ Property / cites work @@
+Termination of nested and mutually recursive algorithms
+Normal rank
@@ Property / cites work @@
+Partial functions in a total setting
@@ Property / cites work: Partial functions in a total setting / rank @@
+Normal rank
@@ Property / cites work @@
+A simple type theory with partial functions and subtypes
+Normal rank
@@ Property / cites work @@
+A general formulation of simultaneous inductive-recursive definitions in type theory
+Normal rank
@@ Property / cites work @@
+The calculus of constructions
@@ Property / cites work: The calculus of constructions / rank @@
+Normal rank
@@ Property / cites work @@
+Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1017/s0960129514000115
+Normal rank
@@ Property / OpenAlex ID @@
+W2023353691
@@ Property / OpenAlex ID: W2023353691 / rank @@
+Normal rank
@@ links / mardi / name / links / mardi / name @@
+Publication:5741556