Foreword to the special focus on formal proofs for mathematics and computer science

DOI10.1007/S11786-014-0214-9zbMATH Open1308.00050OpenAlexW2086038140MaRDI QIDQ2018656FDOQ2018656

Authors:

Publication date: 25 March 2015

Published in: Mathematics in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11786-014-0214-9

Recommendations

• Formal proof -- theory and practice
• Preface to the special issue: Interactive theorem proving and the formalization of mathematics
• Proving and programming
• Writing programs that construct proofs
• Autarkic computations in formal proofs

Mathematics Subject Classification ID

Collections of articles of miscellaneous specific interest (00B15) Proceedings, conferences, collections, etc. pertaining to computer science (68-06)

Cites Work

• Compositional CompCert
• Homotopy type theory. Univalent foundations of mathematics
• HOL with definitions: semantics, soundness, and a verified implementation
• Concrete semantics. With Isabelle/HOL
• Formal proof - the four color theorem
• CakeML
• A machine-checked proof of the odd order theorem
• Formalizing an analytic proof of the prime number theorem

Cited In (11)

• Zen and the art of formalisation
• Social processes, program verification and all that
• Mathematical Knowledge Management
• Developments in formal proofs
• Mathematical Knowledge Management
• Writing programs that construct proofs
• Special issue: Formal proof
• The relationship of derivations in artificial languages to ordinary rigorous mathematical proof
• Formal proof -- theory and practice
• Proof assistants: history, ideas and future
• Mathematics and the formal turn

Uses Software

• Sledgehammer
• CakeML
• CompCert
• Flyspeck
• seL4
• kepler98

This page was built for publication: Foreword to the special focus on formal proofs for mathematics and computer science

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