Working with Mathematical Structures in Type Theory

DOI10.1007/978-3-540-68103-8_11MaRDI QIDQ3499757zbMATH OpenOpenAlexFDO

Authors Claudio Sacerdoti Coen, Enrico Tassi

Publication date 3 June 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-68103-8_11

Mathematics Subject Classification ID

Recommendations

• Packaging Mathematical Structures
• A constructive algebraic hierarchy in Coq.
• Type classes for mathematics in type theory
• On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory
• Developing the algebraic hierarchy with type classes in Coq

Cites work

• A general formulation of simultaneous inductive-recursive definitions in type theory
• Coercive subtyping
• Coercive subtyping for the calculus of constructions (extended abstract)
• Dependently typed records in type theory
• scientific article; zbMATH DE number 1302055 (Why is no real title available?)
• scientific article; zbMATH DE number 2182489 (Why is no real title available?)
• Implicit coercions in type systems
• Mathematical Knowledge Management
• The Four Colour Theorem: Engineering of a Formal Proof

Cited in

(14)

• A constructive algebraic hierarchy in Coq.
• Organizing numerical theories using axiomatic type classes
• Implementing Euclid's straightedge and compass constructions in type theory
• scientific article; zbMATH DE number 1670760 (Why is no real title available?)
• Type classes for mathematics in type theory
• Hints in Unification
• Packaging Mathematical Structures
• Manifest Fields and Module Mechanisms in Intensional Type Theory
• scientific article; zbMATH DE number 2085174 (Why is no real title available?)
• An Interactive Driver for Goal-directed Proof Strategies
• Interfacing Coq + SSReflect with GAP
• The Matita interactive theorem prover
• Implementing type theory in higher order constraint logic programming
• scientific article; zbMATH DE number 2217814 (Why is no real title available?)

Describes a project that uses

Uses Software

• C-CoRN

This page was built for publication: Working with Mathematical Structures in Type Theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3499757)