Pages that link to "Item:Q703860"

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 45 items.

• Coalgebras as Types Determined by Their Elimination Rules (Q5253935) (← links)
• An Assertional Proof of the Stability and Correctness of Natural Mergesort (Q5277907) (← links)
• Mtac: A monad for typed tactic programming in Coq (Q5371944) (← links)
• Idris, a general-purpose dependently typed programming language: Design and implementation (Q5398331) (← links)
• Fast and correctly rounded logarithms in double-precision (Q5444104) (← links)
• Mechanical Theorem Proving in Tarski’s Geometry (Q5453489) (← links)
• On Correctness of Mathematical Texts from a Logical and Practical Point of View (Q5505538) (← links)
• Automatically inferring loop invariants via algorithmic learning (Q5740643) (← links)
• A univalent formalization of the <i>p</i>-adic numbers (Q5740654) (← links)
• Partiality and recursion in interactive theorem provers – an overview (Q5741556) (← links)
• An extensible approach to session polymorphism (Q5741569) (← links)
• A case-study in algebraic manipulation using mechanized reasoning tools (Q5747731) (← links)
• Calculational relation-algebraic proofs in the teaching tool \textsc{CalcCheck} (Q5919026) (← links)
• Synchronous gathering without multiplicity detection: a certified algorithm (Q5920218) (← links)
• Verifying safety critical task scheduling systems in PPTL axiom system (Q5963639) (← links)
• Fundamentals of compositional rewriting theory (Q6052944) (← links)
• Folding left and right matters: Direct style, accumulators, and continuations (Q6099203) (← links)
• An automatically verified prototype of the Android permissions system (Q6103592) (← links)
• Formalizing Some “Small” Finite Models of Projective Geometry in Coq (Q6108812) (← links)
• Machine Learning for Inductive Theorem Proving (Q6108816) (← links)
• Formal verification of termination criteria for first-order recursive functions (Q6149593) (← links)
• Efficient computation of arbitrary control dependencies (Q6165552) (← links)
• Region-based resource management and lexical exception handlers in continuation-passing style (Q6166801) (← links)
• (Q6198042) (← links)
• Verified Runtime Assertion Checking for Memory Properties (Q6487262) (← links)
• Abstract interpretation of recursive logic definitions for efficient runtime assertion checking (Q6535334) (← links)
• A living monograph for graph transformation (Q6535522) (← links)
• Satisfiability modulo finite fields (Q6535532) (← links)
• \textsc{CoqCryptoLine}: a verified model checker with certified results (Q6535536) (← links)
• Comparative verification of the digital library of mathematical functions and computer algebra systems (Q6535563) (← links)
• Automated tail bound analysis for probabilistic recurrence relations (Q6535678) (← links)
• Bounded verification for finite-field-blasting. In a compiler for zero knowledge proofs (Q6535685) (← links)
• Certified verification for algebraic abstraction (Q6535691) (← links)
• Machine learning and information theory concepts towards an AI mathematician (Q6554714) (← links)
• A monadic second-order version of Tarski's geometry of solids (Q6559162) (← links)
• An algebraic approach to simulation and verification for cyber-physical systems with shared-variable concurrency (Q6561342) (← links)
• Uncertainty in runtime verification: a survey (Q6580686) (← links)
• Kripke-Joyal forcing for type theory and uniform fibrations (Q6586829) (← links)
• Accurate calculation of Euclidean norms using double-word arithmetic (Q6599993) (← links)
• Reductive logic, proof-search, and coalgebra: a perspective from resource semantics (Q6612799) (← links)
• Maude2Lean: theorem proving for Maude specifications using Lean (Q6643468) (← links)
• Bouncing threads for circular and non-wellfounded proofs. Towards compositionality with circular proofs (Q6649500) (← links)
• Single-set cubical categories and their formalisation with a proof assistant (Q6653090) (← links)
• Spreads and packings of PG(3,2), formally! (Q6653965) (← links)
• Two new ways to formally prove Dandelin-Gallucci's theorem (Q6666520) (← links)