Working with Mathematical Structures in Type Theory
From MaRDI portal
Publication:3499757
DOI10.1007/978-3-540-68103-8_11zbMATH Open1138.68529OpenAlexW1569206238MaRDI QIDQ3499757FDOQ3499757
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
Recommendations
Cites Work
- Mathematical Knowledge Management
- The Four Colour Theorem: Engineering of a Formal Proof
- A general formulation of simultaneous inductive-recursive definitions in type theory
- Coercive subtyping
- Dependently typed records in type theory
- Title not available (Why is that?)
- Coercive subtyping for the calculus of constructions (extended abstract)
- Implicit coercions in type systems
- Title not available (Why is that?)
Cited In (14)
- Hints in Unification
- Type classes for mathematics in type theory
- Manifest Fields and Module Mechanisms in Intensional Type Theory
- Title not available (Why is that?)
- Title not available (Why is that?)
- Organizing numerical theories using axiomatic type classes
- A constructive algebraic hierarchy in Coq.
- Implementing Euclid's straightedge and compass constructions in type theory
- Packaging Mathematical Structures
- Interfacing Coq + SSReflect with GAP
- Implementing type theory in higher order constraint logic programming
- Title not available (Why is that?)
- The Matita interactive theorem prover
- An Interactive Driver for Goal-directed Proof Strategies
Uses Software
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)
