Canonical Structures for the Working Coq User

DOI10.1007/978-3-642-39634-2_5zbMath1317.68221OpenAlexW10165608MaRDI QIDQ5327334

Assia Mahboubi, Enrico Tassi

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

Mathematics Subject Classification ID

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

• Coq

This page was built for publication: Canonical Structures for the Working Coq User