University of Cambridge > Talks.cam > Computer Laboratory Wednesday Seminars > GLOBULAR: A PROOF ASSISTANT FOR DIAGRAMMATIC SCIENCE

GLOBULAR: A PROOF ASSISTANT FOR DIAGRAMMATIC SCIENCE

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact David Greaves.

Across computer science, physics and mathematics, diagrammatic techniques—-in which formal proofs are represented as a sequence of images, rather than strings of symbols—-are becoming increasingly popular. This raises a number of problems: how can we encode these diagrams combinatorially, and use computers to generate and manipulate them, as well as verify the proof we construct? I will present web-based a new proof assistant, GLOBULAR , that aims to make diagrammatic techniques easy to use. This talk will be given at an accessible level, and will include a demonstration—-bring your laptop and follow along!

This talk is part of the Computer Laboratory Wednesday Seminars series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity