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.
- Category theory, logic and formal linguistics: some connections, old and new (Q280832) (← links)
- A model of type theory in simplicial sets. A brief introduction to Voevodsky's homotopy type theory (Q280837) (← links)
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- Towards a certified version of the encyclopedia of triangle centers (Q294378) (← links)
- Floating-point arithmetic on the test bench. How are verified numerical solutions calculated? (Q335016) (← links)
- A two-valued logic for properties of strict functional programs allowing partial functions (Q352946) (← links)
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program (Q352952) (← links)
- A complete proof system for propositional projection temporal logic (Q391223) (← links)
- A scalable module system (Q391632) (← links)
- Intuitionistic completeness of first-order logic (Q392280) (← links)
- Formal specification and proofs for the topology and classification of combinatorial surfaces (Q396466) (← links)
- \(\lim +, \delta^+\), and non-permutability of \(\beta\)-steps (Q429596) (← links)
- Experiments in program verification using Event-B (Q432154) (← links)
- The area method. A recapitulation (Q437042) (← links)
- Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax (Q438569) (← links)
- A case study in formalizing projective geometry in Coq: Desargues theorem (Q448975) (← links)
- Designing and proving correct a convex hull algorithm with hypermaps in Coq (Q448980) (← links)
- Verification conditions for source-level imperative programs (Q465685) (← links)
- Recycling proof patterns in Coq: case studies (Q475385) (← links)
- Impossibility of gathering, a certification (Q483063) (← links)
- Formal study of functional orbits in finite domains (Q483296) (← links)
- A language-independent proof system for full program equivalence (Q510898) (← links)
- A framework for developing stand-alone certifiers (Q530847) (← links)
- Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving (Q617922) (← links)
- Trace-based verification of imperative programs with I/O (Q617977) (← links)
- Map fusion for nested datatypes in intensional type theory (Q627204) (← links)
- Effective homology of bicomplexes, formalized in Coq (Q631755) (← links)
- Coalgebras in functional programming and type theory (Q639643) (← links)
- Representing model theory in a type-theoretical logical framework (Q654913) (← links)
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (Q670699) (← links)
- Cut branches before looking for bugs: certifiably sound verification on relaxed slices (Q682366) (← links)
- Floating-point arithmetic in the Coq system (Q714617) (← links)
- ``Backward'' coinduction, Nash equilibrium and the rationality of escalation (Q715039) (← links)
- Implementing type systems for the IDE with Xsemantics (Q739624) (← links)
- Implementing geometric algebra products with binary trees (Q742367) (← links)
- A formal proof of the deadline driven scheduler in PPTL axiomatic system (Q744103) (← links)
- An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps (Q839032) (← links)
- Coq formalization of the higher-order recursive path ordering (Q843949) (← links)
- A minimalistic look at widening operators (Q848744) (← links)
- 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 complete axiom system for propositional projection temporal logic with cylinder computation model (Q896162) (← links)
- Sorting nine inputs requires twenty-five comparisons (Q899586) (← 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)
