The Life and Times of JAPE: just another proof editor?

Bernard Sufrin

Peter O'Hearn

FACS Annual General Meeting, followed by the annual FACS Peter Landin Semantics Seminar, delivered by Bernard Sufrin, University of Oxford, and Peter O'Hearn, University College London.

Jape is a configurable proof calculator. It supports the interactive discovery of formal proofs in (more or less arbitrary) inference systems. And it supports the straightforward description of systems of inference rules, and of users' interactions with those rules.

It started life as a hobbyist project (promising no more than insight) in the early 1990s when Richard visited me for a sabbatical in Oxford. It is still distributed, and still used in logic teaching. I will demonstrate the present version and talk about Richard's contribution briefly.

Bernard Sufrin has taught at Oxford since 1978. An Emeritus Fellow of Worcester College and of the Department of Computer Science, he still teaches at Magdalen College and supervises occasional projects.

Peter O'Hearn is a researcher at Meta Superintelligence Labs and a Professor at University College London. He developed Separation Logic and Incorrectness Logic, which underpin tools like Infer, used to detect hundreds of thousands of bugs at Facebook, Microsoft, and Amazon. He co-founded Monoidics (acquired by Facebook) and is a Fellow of the Royal Society and recipient of the Gödel Prize.

Our events are for adults aged 16 years and over.

This meeting is conducted in accordance with the BCS Code of Conduct for Meetings.

BCS is a membership organisation. If you enjoy this event, please consider joining BCS. You’ll be very welcome. You’ll receive access to many exclusive career development tools, an introduction to a thriving professional community and also help us Make IT Good For Society.

If you are attending in person, please familiarise yourself with the Visitor Instructions for the BCS London Office.

Please note, if you have any accessibility needs, please let us know via [email protected], and we’ll work with you to make suitable arrangements.

BCS privacy notice: your data will be processed by BCS in accordance with our data privacy notice.

Photography: by attending this event, you may be photographed or filmed. Please speak to a member of staff if you do not wish to be included.

For overseas delegates who wish to attend the event, please note that BCS does not issue invitation letters.

This event is brought to you by: FACS (Formal Aspects of Computing Science) specialist group

Event venue & nearby stays

BCS, The Chartered Institute for IT, 25 Copthall Ave, London, United Kingdom

Concerts, fests, parties, meetups — all the happenings, one place.

Get the app →

Discover more events by tag