On the Structure of Mizar Types

DOI10.1016/S1571-0661(04)80758-8MaRDI QIDQ4924547zbMATH OpenFDO

Authors Grzegorz Bancerek

Publication date 6 June 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S1571-0661(04)80758-8

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• On the ubiquity of certain total type structures
• scientific article; zbMATH DE number 4050952
• Types and coalgebraic structure
• scientific article; zbMATH DE number 1070622
• A modular construction of type theories
• On the internal structures of inductive types
• Model structures on categories of models of type theories
• A Type Theory with Mixed Constructivity and Assignments
• scientific article; zbMATH DE number 1014760
• On integral structure types

Cites work

• A compendium of continuous lattices in MIZAR
• A refinement of de Bruijn's formal language of mathematics
• Commutative algebra in the Mizar system
• scientific article; zbMATH DE number 1951639 (Why is no real title available?)
• scientific article; zbMATH DE number 1951640 (Why is no real title available?)
• scientific article; zbMATH DE number 1863397 (Why is no real title available?)
• On equivalents of well-foundedness. An experiment in MIZAR

Cited in

(8)

• Flexary connectives in Mizar
• The Mizar Mathematical Library in OMDoc: translation and applications
• Pythagorean tuning: pentatonic and heptatonic scale
• Presentation and manipulation of Mizar properties in an Isabelle object logic
• User interaction with the Matita proof assistant
• Formalising foundations of mathematics
• Mizar’s Soft Type System
• Alternative Aggregates in Mizar

Describes a project that uses

Uses Software

• Mizar

This page was built for publication: On the Structure of Mizar Types

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