Pages that link to "Item:Q703860"
From MaRDI portal
The following pages link to Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. (Q703860):
Displaying 50 items.
- Tests and Proofs for Enumerative Combinatorics (Q2827441) (← links)
- Mechanical Verification of a Constructive Proof for FLP (Q2829253) (← links)
- From Types to Sets by Local Type Definitions in Higher-Order Logic (Q2829259) (← links)
- Semantic determinism and functional logic program properties (Q2864514) (← links)
- Tool support for proof engineering (Q2867938) (← links)
- Automated formal analysis and verification: an overview (Q2871577) (← links)
- Inductive and coinductive components of corecursive functions in Coq (Q2873661) (← links)
- Let’s See How Things Unfold: Reconciling the Infinite with the Intensional (Extended Abstract) (Q2888481) (← links)
- Towards Logical Frameworks in the Heterogeneous Tool Set Hets (Q2890328) (← links)
- Automating Induction with an SMT Solver (Q2891425) (← links)
- Deciding Regular Expressions (In-)Equivalence in Coq (Q2915138) (← links)
- Type theory and formal proof. An introduction (Q2925448) (← links)
- Deletion: The curse of the red-black tree (Q2933113) (← links)
- Homotopy type theory and Voevodsky’s univalent foundations (Q2933829) (← links)
- A Consistent Foundation for Isabelle/HOL (Q2945636) (← links)
- Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language (Q2947456) (← links)
- UTPCalc — A Calculator for UTP Predicates (Q2971182) (← links)
- Formalization of real analysis: a survey of proof assistants and libraries (Q2973239) (← links)
- Friends with Benefits (Q2988636) (← links)
- Comprehending Isabelle/HOL’s Consistency (Q2988665) (← links)
- On Choice Rules in Dependent Type Theory (Q2988806) (← links)
- MikiBeta : A General GUI Library for Visualizing Proof Trees (Q3003488) (← links)
- Balancing weight-balanced trees (Q3016214) (← links)
- Partial Derivative Automata Formalized in Coq (Q3073622) (← links)
- Structural Analysis of Narratives with the Coq Proof Assistant (Q3087995) (← links)
- Formal proofs for theoretical properties of Newton's method (Q3094171) (← links)
- A formal study of Bernstein coefficients and polynomials (Q3094174) (← links)
- Type classes for mathematics in type theory (Q3094177) (← links)
- A pluralist approach to the formalisation of mathematics (Q3094181) (← links)
- Hardware-Dependent Proofs of Numerical Programs (Q3100216) (← links)
- A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry (Q3102734) (← links)
- Introduction to Model Checking (Q3176359) (← links)
- Combining Model Checking and Deduction (Q3176378) (← links)
- Bisimulations Generated from Corecursive Equations (Q3178257) (← links)
- Extracting a DPLL Algorithm (Q3178287) (← links)
- A Brief Overview of Agda – A Functional Language with Dependent Types (Q3183520) (← links)
- Acyclic Preferences and Existence of Sequential Nash Equilibria: A Formal and Constructive Equivalence (Q3183536) (← links)
- Trace-Based Coinductive Operational Semantics for While (Q3183540) (← links)
- Formal Verification of Exact Computations Using Newton’s Method (Q3183542) (← links)
- Para-Disagreement Logics and Their Implementation Through Embedding in Coq and SMT (Q3305339) (← links)
- From Mathesis Universalis to Provability, Computability, and Constructivity (Q3305633) (← links)
- Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof (Q3453106) (← links)
- SEPIA: Search for Proofs Using Inferred Automata (Q3454097) (← links)
- Inductive Beluga: Programming Proofs (Q3454100) (← links)
- Rationality Authority for Provable Rational Behavior (Q3464466) (← links)
- Mechanized Verification of CPS Transformations (Q3498467) (← links)
- CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types (Q3499747) (← links)
- In the Search of a Naive Type Theory (Q3499754) (← links)
- A Short Presentation of Coq (Q3543643) (← links)
- Canonical Big Operators (Q3543652) (← links)
