An approach to literate and structured formal developments

DOI10.1007/BF01211052MaRDI QIDQ1911317zbMATH OpenOpenAlexFDO

Authors Martin Simons, Matthias Weber

Publication date 13 August 1996

Published in Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/bf01211052

zbMATH Keywords

literate programmingformal developmentsrevision management system

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27)

Recommendations

• scientific article; zbMATH DE number 1024410
• Communicating formal proofs: the case of Flyspeck
• Mathematical Knowledge Management
• The generic development language. Presentation and case studies
• Structured formal development in Isabelle

Cites work

• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 46957 (Why is no real title available?)
• scientific article; zbMATH DE number 48517 (Why is no real title available?)
• scientific article; zbMATH DE number 51473 (Why is no real title available?)
• scientific article; zbMATH DE number 1331926 (Why is no real title available?)
• scientific article; zbMATH DE number 482967 (Why is no real title available?)
• scientific article; zbMATH DE number 595218 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• scientific article; zbMATH DE number 194916 (Why is no real title available?)
• scientific article; zbMATH DE number 4115920 (Why is no real title available?)
• scientific article; zbMATH DE number 789390 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• A framework for defining logics
• An overview of the Tecton proof system
• Definition and basic properties of the Deva meta-calculus
• Experimenting with Isabelle in ZF set theory
• FME '94: industrial benefit of formal methods. 2nd international symposium of formal methods Europe, Barcelona, Spain, October 24--28, 1994. Proceedings
• Fixed point theorems and semantics: A folk tale
• IMPS: An interactive mathematical proof system
• Literate Programming
• On the shape of mathematical arguments
• Set theory for verification. I: From foundations to functions
• Specification of the UNIX Filing System
• The calculus of constructions
• The generic development language. Presentation and case studies

Cited in

(3)

• Mathematical Knowledge Management
• Communicating formal proofs: the case of Flyspeck
• Towards a theory of document structure

Describes a project that uses

Uses Software

• Tecton
• CalcCheck
• IMPS
• Nuprl
• Isabelle/ZF

This page was built for publication: An approach to literate and structured formal developments

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