Exploring abstract algebra in constructive type theory

DOI10.1007/3-540-58156-1_43zbMath1433.68553OpenAlexW1530552858MaRDI QIDQ5210799

No author found.

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) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

Innovations in computational type theory using Nuprl ⋮ Towards the Mathematics Software Bus ⋮ A two-level approach towards lean proof-checking ⋮ The control layer in open mechanized reasoning systems: Annotations and tactics

Uses Software

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

Cites Work

• A course in constructive algebra
• Implementing constructive real analysis (preliminary report)
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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