scientific article
From MaRDI portal
Publication:3075246
zbMath1211.68368MaRDI QIDQ3075246
Georges Gonthier, Assia Mahboubi
Publication date: 10 February 2011
Full work available at URL: http://jfr.cib.unibo.it/article/view/1979
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (34)
Proof mining with dependent types ⋮ Eisbach: a proof method language for Isabelle ⋮ Unnamed Item ⋮ An intuitionistic proof of a discrete form of the Jordan curve theorem formalized in Coq with combinatorial hypermaps ⋮ Packaging Mathematical Structures ⋮ Trace-Based Coinductive Operational Semantics for While ⋮ Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis ⋮ Hammer for Coq: automation for dependent type theory ⋮ Foundations of dependent interoperability ⋮ Proof-Producing Reflection for HOL ⋮ Foundational Property-Based Testing ⋮ A Certified Reduction Strategy for Homological Image Processing ⋮ Computational Complexity Via Finite Types ⋮ Formalising Mathematics in Simple Type Theory ⋮ Unnamed Item ⋮ Certifying assembly with formal security proofs: the case of BBS ⋮ Designing and proving correct a convex hull algorithm with hypermaps in Coq ⋮ A Short Presentation of Coq ⋮ Canonical Big Operators ⋮ Recycling proof patterns in Coq: case studies ⋮ Formalization of the Domination Chain with Weighted Parameters (Short Paper) ⋮ Partiality, State and Dependent Types ⋮ From LCF to Isabelle/HOL ⋮ Incidence Simplicial Matrices Formalized in Coq/SSReflect ⋮ From Sets to Bits in Coq ⋮ A formalization of multi-tape Turing machines ⋮ Point-Free, Set-Free Concrete Linear Algebra ⋮ Some Wellfounded Trees in UniMath ⋮ Finite Groups Representation Theory with Coq ⋮ A Decision Procedure for Regular Expression Equivalence in Type Theory ⋮ Coquet: A Coq Library for Verifying Hardware ⋮ Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers ⋮ Theorem of three circles in Coq ⋮ Formally verified certificate checkers for hardest-to-round computation
Uses Software
This page was built for publication:
