Canonical structures for the working Coq user
From MaRDI portal
Recommendations
Cited in
(24)- Session types without sophistry. System description
- A formalization of Dedekind domains and class groups of global fields
- Exploring the structure of an algebra text with locales
- Classification of finite fields with applications
- A mechanized textbook proof of a type unification algorithm
- An introduction to small scale reflection in Coq
- Hints in Unification
- 1ML -- core and modules united
- Type inference in mathematics
- Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
- Validating Mathematical Structures
- Formalizing the Face Lattice of Polyhedra
- Formalizing the face lattice of polyhedra
- A trustful monad for axiomatic reasoning with probability and nondeterminism
- Formalization techniques for asymptotic reasoning in classical analysis
- Implementing type theory in higher order constraint logic programming
- Mathematical Knowledge Management
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
- A formal proof of the irrationality of (3)
- scientific article; zbMATH DE number 7649978 (Why is no real title available?)
- Integration of multiple formal matrix models in Coq
- Mathematical structures in dependent type theory (invited talk)
- Hierarchy builder: algebraic hierarchies made easy in Coq with Elpi (system description)
- Translating HOL-Light proofs to Coq
This page was built for publication: Canonical structures for the working Coq user
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5327334)
