Canonical Structures for the Working Coq User
From MaRDI portal
Publication:5327334
DOI10.1007/978-3-642-39634-2_5zbMath1317.68221OpenAlexW10165608MaRDI QIDQ5327334
Publication date: 7 August 2013
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-00816703/file/main.pdf
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (17)
Unnamed Item ⋮ Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis ⋮ Validating Mathematical Structures ⋮ Formalizing the Face Lattice of Polyhedra ⋮ Unnamed Item ⋮ Integration of multiple formal matrix models in Coq ⋮ Unnamed Item ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading ⋮ Exploring the structure of an algebra text with locales ⋮ 1ML – Core and modules united ⋮ A trustful monad for axiomatic reasoning with probability and nondeterminism ⋮ Formalization of the fundamental group in untyped set theory using auto2 ⋮ Unnamed Item ⋮ Session types without sophistry. System description ⋮ Implementing type theory in higher order constraint logic programming ⋮ Classification of finite fields with applications ⋮ A formalization of Dedekind domains and class groups of global fields
Uses Software
This page was built for publication: Canonical Structures for the Working Coq User
