Graphical Theories of Interactive Systems: Can a Proof Assistant Help?

Robin Milner

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Computer scientists are privileged, or doomed, to deal rigorously with large structures. This happens, of course, with hardware design and verification, and with programs and specifications. Considerable progress has been made with mechanised proof assistance for both. Going further into the back room, programming languages are also big structures. It’s very uncommon to have help from a proof assistant while actually designing a language, probably because the very formalism for writing down what a language means is changing under our feet, so it’s asking too much for those who build proof assistants to keep up with these developments enough to help the designers in real time. All the same, it has been encouraging to see plenty of post hoc verification of properties of Standard ML using its semantic formalism. Perhaps a future language design using “big step structure operational semantics” could be done using proof assistance to check out the sanity of a large set of inference rules before they are frozen into a design.
Original languageEnglish
Title of host publicationTheorem Proving in Higher Order Logics
Subtitle of host publication13th International Conference, TPHOLs 2000 Portland, OR, USA, August 14–18, 2000 Proceedings
PublisherSpringer Berlin Heidelberg
Pages442
Number of pages1
Volume1869
ISBN (Electronic)978-3-540-44659-0
ISBN (Print)978-3-540-67863-2
DOIs
Publication statusPublished - 2000

Fingerprint

Dive into the research topics of 'Graphical Theories of Interactive Systems: Can a Proof Assistant Help?'. Together they form a unique fingerprint.

Cite this