An approach to literate and structured formal developments

DOI10.1007/BF01211052zbMath0843.68111OpenAlexW2007962263MaRDI QIDQ1911317

Matthias Weber, Martin Simons

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)

Uses Software

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

Cites Work

• Definition and basic properties of the Deva meta-calculus
• The generic development language. Presentation and case studies
• The calculus of constructions
• Fixed point theorems and semantics: A folk tale
• On the shape of mathematical arguments
• Experimenting with Isabelle in ZF set theory
• Set theory for verification. I: From foundations to functions
• IMPS: An interactive mathematical proof system
• FME '94: industrial benefit of formal methods. 2nd international symposium of formal methods Europe, Barcelona, Spain, October 24--28, 1994. Proceedings
• An overview of the Tecton proof system
• Specification of the UNIX Filing System
• Literate Programming
• A framework for defining logics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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