Exploring abstract algebra in constructive type theory

DOI10.1007/3-540-58156-1_43MaRDI QIDQ5210799zbMATH OpenOpenAlexFDO

Authors

Publication date 21 January 2020

Published in Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-58156-1_43

Mathematics Subject Classification ID

Free semigroups, generators and relations, word problems (20M05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Developing the algebraic hierarchy with type classes in Coq
• scientific article; zbMATH DE number 3986665
• scientific article; zbMATH DE number 1759393
• Nuprl's class theory and its applications
• Implementing constructive real analysis (preliminary report)

Cites work

• A course in constructive algebra
• scientific article; zbMATH DE number 3859117 (Why is no real title available?)
• scientific article; zbMATH DE number 3986665 (Why is no real title available?)
• scientific article; zbMATH DE number 107769 (Why is no real title available?)
• scientific article; zbMATH DE number 1331927 (Why is no real title available?)
• scientific article; zbMATH DE number 517013 (Why is no real title available?)
• scientific article; zbMATH DE number 517385 (Why is no real title available?)
• scientific article; zbMATH DE number 3440338 (Why is no real title available?)
• Implementing constructive real analysis (preliminary report)

Cited in

(9)

• Towards the Mathematics Software Bus
• Implementing Euclid's straightedge and compass constructions in type theory
• Nuprl's class theory and its applications
• A two-level approach towards lean proof-checking
• Towards Constructive Homological Algebra in Type Theory
• The control layer in open mechanized reasoning systems: Annotations and tactics
• Set theory, higher order logic or both?
• Importing mathematics from HOL into Nuprl
• Innovations in computational type theory using Nuprl

Describes a project that uses

Uses Software

• AXIOM
• HOL
• Analytica
• Nuprl
• LARCH
• LEGO

This page was built for publication: Exploring abstract algebra in constructive type theory

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