Modular structures as dependent types in Isabelle

DOI10.1007/3-540-48167-2_9MaRDI QIDQ4944854zbMATH OpenFDO

Authors Florian Kammüller

Publication date 22 March 2000

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48167-2_9

zbMATH Keywords

Isabelle

Mathematics Subject Classification ID

Recommendations

• Modular reasoning in Isabelle
• scientific article; zbMATH DE number 1187955
• A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
• Exploring the structure of an algebra text with locales
• Modelling algebraic structures and morphisms in ACL2

Cited in

(12)

• A formal proof of Sylow's theorem. An experiment in abstract algebra with Isabelle H0L
• A modular first formalisation of combinatorial design theory
• Exploring the structure of an algebra text with locales
• Modelling algebraic structures and morphisms in ACL2
• Locales: a module system for mathematical theories
• Modular reasoning in Isabelle
• Dependently typed records for representing mathematical structure
• Structured formal development with quotient types in Isabelle/HOL
• Algebraic structures and dependent records
• Reasoning About Algebraic Structures with Implicit Carriers in Isabelle/HOL
• Modeling abstract types in modules with open existential types
• Multiple-inheritance hazards in dependently-typed algebraic hierarchies

Describes a project that uses

Uses Software

• Isabelle
• LARCH
• IMPS
• PolyTOIL

This page was built for publication: Modular structures as dependent types in Isabelle

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