scientific article; zbMATH DE number 5850142
From MaRDI portal
Publication:3075246
zbMATH Open1211.68368MaRDI QIDQ3075246FDOQ3075246
Georges Gonthier, Assia Mahboubi
Publication date: 10 February 2011
Full work available at URL: http://jfr.cib.unibo.it/article/view/1979
Title of this publication is not available (Why is that?)
Cited In (37)
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- Designing and proving correct a convex hull algorithm with hypermaps in Coq
- From Sets to Bits in Coq
- Proof reflection in Coq
- An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps
- Finite Groups Representation Theory with Coq
- Foundational Property-Based Testing
- Proof-Producing Reflection for HOL
- Eisbach: a proof method language for Isabelle
- Computational Complexity Via Finite Types
- Formalising Mathematics in Simple Type Theory
- Certifying assembly with formal security proofs: the case of BBS
- Title not available (Why is that?)
- Theorem of three circles in Coq
- A formalization of multi-tape Turing machines
- Coquet: A Coq Library for Verifying Hardware
- A Certified Reduction Strategy for Homological Image Processing
- Proof mining with dependent types
- Some Wellfounded Trees in UniMath
- Recycling proof patterns in Coq: case studies
- Packaging Mathematical Structures
- Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
- Formalization of the Domination Chain with Weighted Parameters (Short Paper)
- From LCF to Isabelle/HOL
- Trace-Based Coinductive Operational Semantics for While
- Formally verified certificate checkers for hardest-to-round computation
- Incidence Simplicial Matrices Formalized in Coq/SSReflect
- Partiality, State and Dependent Types
- Foundations of dependent interoperability
- Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers
- \textsc{CoqCryptoLine}: a verified model checker with certified results
- Certified verification for algebraic abstraction
- Point-Free, Set-Free Concrete Linear Algebra
- Hammer for Coq: automation for dependent type theory
- Title not available (Why is that?)
- A Short Presentation of Coq
- Canonical Big Operators
Uses Software
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3075246)
