First-Class Type Classes

DOI10.1007/978-3-540-71067-7_23MaRDI QIDQ3543665zbMATH OpenOpenAlexFDO

Authors Matthieu Sozeau, Nicolas Oury

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

Mathematics Subject Classification ID

Recommendations

• Type classes for mathematics in type theory
• Constructive Type Classes in Isabelle
• Modular type classes
• Type Reconstruction for Type Classes
• Type classes with more higher-order polymorphism

Cites work

• A compiled implementation of strong reduction
• Associated types with class
• Constructive Type Classes in Isabelle
• scientific article; zbMATH DE number 1629944 (Why is no real title available?)
• scientific article; zbMATH DE number 1670760 (Why is no real title available?)
• scientific article; zbMATH DE number 2061705 (Why is no real title available?)
• Proof theory in computer science. International seminar, PTCS 2001, Dagstuhl Castle, Germany, October 7--12, 2001. Proceedings
• Subset Coercions in Coq
• Theorem Proving in Higher Order Logics

Cited in

(36)

• A consistent foundation for Isabelle/HOL
• Traits: correctness-by-construction for free
• Formally verified certificate checkers for hardest-to-round computation
• A synthetic proof of Pappus' theorem in Tarski's geometry
• Automatic refinement to efficient data structures: a comparison of two approaches
• Two cryptomorphic formalizations of projective incidence geometry
• A consistent foundation for Isabelle/HOL
• Program calculation in Coq
• 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 verifications of termination certificates
• Tactics for Reasoning Modulo AC in Coq
• Hints in Unification
• Packaging Mathematical Structures
• scientific article; zbMATH DE number 3878328 (Why is no real title available?)
• Constructive Type Classes in Isabelle
• First-Class Object Sets
• First-Class Functions
• Foundations of dependent interoperability
• COCHIS: stable and coherent implicits
• Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
• Validating Mathematical Structures
• On the bright side of type classes: instance arguments in Agda
• The Matita interactive theorem prover
• Computer Certified Efficient Exact Reals in Coq
• Certifying dictionary construction in Isabelle/HOL
• Mtac: a monad for typed tactic programming in Coq
• Recent Trends in Algebraic Development Techniques
• scientific article; zbMATH DE number 7649978 (Why is no real title available?)
• Integration of multiple formal matrix models in Coq
• \textsf{LOGIC}: a Coq library for logics
• Mathematical structures in dependent type theory (invited talk)
• Structured monads for generic first-order syntax metatheory
• Use and abuse of instance parameters in the Lean mathematical library.
• Inductive predicates via least fixpoints in higher-order separation logic

Describes a project that uses

Uses Software

• Coq
• Locales
• Simula 67

This page was built for publication: First-Class Type Classes

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