Working with Mathematical Structures in Type Theory
From MaRDI portal
Publication:3499757
DOI10.1007/978-3-540-68103-8_11zbMath1138.68529OpenAlexW1569206238MaRDI QIDQ3499757
Enrico Tassi, Claudio Sacerdoti Coen
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (8)
Hints in Unification ⋮ Packaging Mathematical Structures ⋮ An Interactive Driver for Goal-directed Proof Strategies ⋮ Interfacing Coq + SSReflect with GAP ⋮ The Matita Interactive Theorem Prover ⋮ Manifest Fields and Module Mechanisms in Intensional Type Theory ⋮ Type classes for mathematics in type theory ⋮ Implementing type theory in higher order constraint logic programming
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Dependently typed records in type theory
- Coercive subtyping for the calculus of constructions
- The Four Colour Theorem: Engineering of a Formal Proof
- Coercive subtyping
- A general formulation of simultaneous inductive-recursive definitions in type theory
- Implicit coercions in type systems
- Mathematical Knowledge Management
This page was built for publication: Working with Mathematical Structures in Type Theory
