Type classes for mathematics in type theory

DOI10.1017/S0960129511000119zbMath1223.68105OpenAlexW2164688709MaRDI QIDQ3094177

Eelis van der Weegen, Bas Spitters

Publication date: 21 October 2011

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0960129511000119

zbMATH Keywords

theorem provingCoqbundlingformalized mathematicsalgebraic hierarchyfirst-class type classes

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (13)

Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis ⋮ Validating Mathematical Structures ⋮ Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL ⋮ Synthetic topology in Homotopy Type Theory for probabilistic programming ⋮ Theory Presentation Combinators ⋮ ROSCoq: Robots Powered by Constructive Reals ⋮ Refinement to Certify Abstract Interpretations, Illustrated on Linearization for Polyhedra ⋮ Multiple-inheritance hazards in dependently-typed algebraic hierarchies ⋮ A formal C memory model for separation logic ⋮ Unnamed Item ⋮ Computer Certified Efficient Exact Reals in Coq ⋮ Formalization of universal algebra in Agda ⋮ Modelling algebraic structures and morphisms in ACL2

Uses Software

• AXIOM
• Coq
• CLEAN
• Matita
• C-CoRN

Cites Work

• Dependently typed records in type theory
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Partial Horn logic and Cartesian categories
• A computer-verified monadic functional implementation of the integral
• The calculus of constructions
• A constructive algebraic hierarchy in Coq.
• A type system for computer algebra
• User interaction with the Matita proof assistant
• Hints in Unification
• Packaging Mathematical Structures
• Working with Mathematical Structures in Type Theory
• Certified Exact Transcendental Real Number Computation in Coq
• First-Class Type Classes
• Setoids in type theory
• Extending Coq with Imperative Features and Its Application to SAT Verification

This page was built for publication: Type classes for mathematics in type theory