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):

Displayed 26 items.

• Ordinal arithmetic: Algorithms and mechanization (Q851144) ‎ (← links)
• Innovations in computational type theory using Nuprl (Q865639) ‎ (← links)
• \textit{Theorema}: Towards computer-aided mathematical theory exploration (Q865646) ‎ (← links)
• The ILTP problem library for intuitionistic logic (Q877897) ‎ (← links)
• A mechanized proof of the basic perturbation lemma (Q928666) ‎ (← links)
• Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves (Q928671) ‎ (← links)
• A mechanical analysis of program verification strategies (Q928673) ‎ (← links)
• Formalizing non-interference for a simple bytecode language in Coq (Q931434) ‎ (← links)
• Polyhedra genus theorem and Euler formula: A hypermap-formalized intuitionistic proof (Q944364) ‎ (← links)
• Formal verification of a C-like memory model and its uses for verifying program transformations (Q945054) ‎ (← links)
• Proof synthesis and reflection for linear arithmetic (Q945055) ‎ (← links)
• Optimization techniques for propositional intuitionistic logic and their implementation (Q959821) ‎ (← links)
• A decision procedure for linear ``big O'' equations (Q2642465) ‎ (← links)
• Code-carrying theories (Q2643124) ‎ (← links)
• Mechanizing common knowledge logic using COQ (Q2643149) ‎ (← links)
• Design and formal proof of a new optimal image segmentation program with hypermaps (Q2643883) ‎ (← 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)
• A Machine Checked Soundness Proof for an Intermediate Verification Language (Q3599104) ‎ (← links)
• Formal Modelling of Emotions in BDI Agents (Q3602941) ‎ (← 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)