Validating Mathematical Structures
From MaRDI portal
Publication:5048998
DOI10.1007/978-3-030-51054-1_8OpenAlexW3040202382MaRDI QIDQ5048998
Publication date: 9 November 2022
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2002.00620
Related Items
Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis, Multiple-inheritance hazards in dependently-typed algebraic hierarchies
Uses Software
Cites Work
- Unnamed Item
- Dependently typed records in type theory
- Telescopic mappings in typed lambda calculus
- The calculus of constructions
- The undecidability of the second-order unification problem
- A constructive algebraic hierarchy in Coq.
- Coquelicot: a user-friendly library of real analysis for Coq
- A hierarchy of monadic effects for program verification using equational reasoning
- Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
- Type classes for mathematics in type theory
- Hints in Unification
- Packaging Mathematical Structures
- The Lean Theorem Prover (System Description)
- First-Class Type Classes
- Constructive Type Classes in Isabelle
- Implicit coercions in type systems
- Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis
- The Matita Interactive Theorem Prover
- Canonical Structures for the Working Coq User
- A Machine-Checked Proof of the Odd Order Theorem
- Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
- How to make ad hoc proof automation less ad hoc
