Theories as types

DOI10.1007/978-3-319-94205-6_38MaRDI QIDQ1799118zbMATH OpenOpenAlexFDO

Authors Dennis Müller, Florian Rabe, Michael Kohlhase

Publication date 18 October 2018

Full work available at URL https://doi.org/10.1007/978-3-319-94205-6_38

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Mathematical knowledge management (68V30)

Recommendations

• scientific article; zbMATH DE number 17707
• scientific article; zbMATH DE number 1187955
• Dependently typed records in type theory
• scientific article; zbMATH DE number 1678369
• scientific article; zbMATH DE number 1302055

Cited in

(13)

• Experiences from exporting major proof assistant libraries
• Structuring theories with implicit morphisms
• Essential core of the Hawking–Ellis types
• scientific article; zbMATH DE number 17707 (Why is no real title available?)
• scientific article; zbMATH DE number 1038419 (Why is no real title available?)
• scientific article; zbMATH DE number 2154393 (Why is no real title available?)
• Theory Instantiation
• scientific article; zbMATH DE number 5066367 (Why is no real title available?)
• High-Level Theories
• Extracting theory graphs from Aldor libraries
• Injecting formal mathematics into LaTeX
• Global, regional, and local contexts
• Rapid prototyping formal systems in MMT: 5 case studies

Describes a project that uses

Uses Software

• Mizar
• OpenDreamKit
• Idris
• Coq
• FoCaLiZe
• Isabelle/Isar
• PVS
• HOL Light

This page was built for publication: Theories as types

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