GLOBULAR: A PROOF ASSISTANT FOR DIAGRAMMATIC SCIENCE

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

• Jamie Vicary - Department of Computer Science, University of Oxford
• Wednesday 01 February 2017, 16:15-17:15
• Lecture Theatre 1, Computer Laboratory.

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 Wednesday Seminars - Department of Computer Science and Technology series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Department of Computer Science and Technology talks and seminars
• Graduate-Seminars
• Guy Emerson's list
• Interested Talks
• Lecture Theatre 1, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• Wednesday Seminars - Department of Computer Science and Technology
• bld31
• computer science
• ndk22's list
• ob366-ai4er
• rp587
• se393's list

Note that ex-directory lists are not shown.