First-Class Type Classes
From MaRDI portal
Publication:3543665
DOI10.1007/978-3-540-71067-7_23zbMath1165.68475OpenAlexW1558115254MaRDI QIDQ3543665
Publication date: 4 December 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-71067-7_23
Related Items
A synthetic proof of Pappus' theorem in Tarski's geometry, Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis, Validating Mathematical Structures, Two cryptomorphic formalizations of projective incidence geometry, Hints in Unification, Packaging Mathematical Structures, Traits: correctness-by-construction for free, Foundations of dependent interoperability, A Consistent Foundation for Isabelle/HOL, Automatic refinement to efficient data structures: a comparison of two approaches, Integration of multiple formal matrix models in Coq, \textsf{LOGIC}: a Coq library for logics, Unnamed Item, Mtac: A monad for typed tactic programming in Coq, A consistent foundation for Isabelle/HOL, The Matita Interactive Theorem Prover, Computer Certified Efficient Exact Reals in Coq, Program Calculation in Coq, COCHIS: Stable and coherent implicits, Point-Free, Set-Free Concrete Linear Algebra, Formalising Overlap Algebras in Matita, Type classes for mathematics in type theory, CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, Tactics for Reasoning Modulo AC in Coq, Formally verified certificate checkers for hardest-to-round computation
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A compiled implementation of strong reduction
- Constructive Type Classes in Isabelle
- Subset Coercions in Coq
- Associated types with class
- Theorem Proving in Higher Order Logics
- Proof theory in computer science. International seminar, PTCS 2001, Dagstuhl Castle, Germany, October 7--12, 2001. Proceedings
