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

• Fixpoints and Search in PVS (Q3558967) (← links)
• The dodecahedral conjecture (Q3584349) (← links)
• A Machine Checked Soundness Proof for an Intermediate Verification Language (Q3599104) (← links)
• Formal Modelling of Emotions in BDI Agents (Q3602941) (← links)
• Crafting a Proof Assistant (Q3612433) (← links)
• A Polymorphic Type System for the Lambda-Calculus with Constructors (Q3637198) (← links)
• Combining Coq and Gappa for Certifying Floating-Point Programs (Q3637269) (← links)
• Formal Proof: Reconciling Correctness and Understanding (Q3637280) (← links)
• Finite Groups Representation Theory with Coq (Q3637300) (← links)
• First-Class Object Sets (Q3638247) (← links)
• Using Structural Recursion for Corecursion (Q3638255) (← links)
• A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq (Q3638257) (← links)
• Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus (Q3638285) (← links)
• An induction principle for nested datatypes in intensional type theory (Q3638923) (← links)
• Building Mathematics-Based Software Systems to Advance Science and Create Knowledge (Q3644710) (← links)
• Libraries for Generic Programming in Haskell (Q3649135) (← links)
• Computational logic: its origins and applications (Q4559535) (← links)
• Algebraic data integration (Q4577809) (← links)
• Validating Brouwer's continuity principle for numbers using named exceptions (Q4640313) (← links)
• An insider's look at LF type reconstruction: everything you (n)ever wanted to know (Q4912883) (← links)
• The Strategy Challenge in SMT Solving (Q4913859) (← links)
• Mechanized Verification of Computing Dominators for Formalizing Compilers (Q4916051) (← links)
• Common Knowledge Logic in a Higher Order Proof Assistant (Q4916081) (← links)
• Implementing Real Numbers With RZ (Q4918049) (← links)
• Folding left and right over Peano numbers (Q4972067) (← links)
• A Formal, Resource Consumption-Preserving Translation from Actors with Cooperative Scheduling to Haskell* (Q4988924) (← links)
• (Q4989394) (← links)
• (Q5014449) (← links)
• (Q5015189) (← links)
• A focused linear logical framework and its application to metatheory of object logics (Q5022931) (← links)
• A Formalization of Properties of Continuous Functions on Closed Intervals (Q5041063) (← links)
• Semantic Foundations for Deterministic Dataflow and Stream Processing (Q5041103) (← links)
• Deep Generation of Coq Lemma Names Using Elaborated Terms (Q5048996) (← links)
• Fold–unfold lemmas for reasoning about recursive programs using the Coq proof assistant (Q5051990) (← links)
• Getting There and Back Again (Q5074057) (← links)
• Characteristics of de Bruijn’s early proof checker Automath (Q5089679) (← links)
• (Q5109521) (← links)
• Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting (Q5164173) (← links)
• Simulating Finite Eilenberg Machines with a Reactive Engine (Q5166624) (← links)
• Verified Compilation and the B Method: A Proposal and a First Appraisal (Q5179355) (← links)
• Introduction to Type Theory (Q5191087) (← links)
• Dependent Types at Work (Q5191088) (← links)
• Structural Abstract Interpretation: A Formal Study Using Coq (Q5191090) (← links)
• Proof Auditing Formalised Mathematics (Q5195266) (← links)
• Incidence Simplicial Matrices Formalized in Coq/SSReflect (Q5200106) (← links)
• Computer Certified Efficient Exact Reals in Coq (Q5200110) (← links)
• A Foundational View on Integration Problems (Q5200111) (← links)
• The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem (Q5204803) (← links)
• Axiomatic and dual systems for constructive necessity, a formally verified equivalence (Q5231279) (← links)
• Program Testing and the Meaning Explanations of Intuitionistic Type Theory (Q5253930) (← links)