A language with type-dependent equality

DOI10.1007/978-3-030-81097-9_18zbMath1485.68293OpenAlexW3186568737MaRDI QIDQ2128827

Florian Rabe

Publication date: 22 April 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-81097-9_18

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20) Type theory (03B38)

Uses Software

• Coq
• GAP
• SageMath
• PVS
• Mizar
• HOL
• Lean

Cites Work

• Unnamed Item
• Innovations in computational type theory using Nuprl
• A survey of languages for formalizing mathematics
• The Lean Theorem Prover (System Description)