Scottish Theorem Proving Seminar
Date/Time
5th December 2014
1.15 pm: lunch provided by SICSA
2.00 - 5.00 pm: talks
Location
Room 422
Sir Alwyn Williams Building
University of Glasgow
18 Lilybank Gardens
Glasgow, G12 8RZ
Registration
Programme
1.15 - 2.00 pm Lunch
2.00 - 2.40 pm Simon Gay University of Glasgow Automated Verification of Quantum Protocols
2.40 - 3.20 pm Roy Dyckhoff University of St Andrews Geometrisation of First-Order Logic
3.20 - 3.40 pm Coffee Break
3.40 - 4.20 pm Phil Scott University of Edinburgh The Polygonal Jordan Curve Theorem without Ruler or Compass
4.20 - 5.00 pm James McKinna University of Edinburgh On the Sato et al. map-skeleton representation of lambda terms
5.00 pm Close
Abstract
Automated Verification of Quantum Protocols
Simon Gay
We present a tool which uses a concurrent language for describing quantum systems, and performs verification by checking equivalence between specification and implementation. In general, simulation of quantum systems using current computing technology is infeasible. We restrict ourselves to the stabilizer formalism, in which there are efficient simulation algorithms. In particular, we consider concurrent quantum protocols that behave functionally in the sense of computing a deterministic input-output relation for all interleavings of the concurrent system. Crucially, these input-output relations can be abstracted by superoperators, enabling us to take advantage of linearity. This allows us to analyse the behaviour of protocols with arbitrary input, by simulating their operation on a finite basis set consisting of stabilizer states. Despite the limitations of the stabilizer formalism and also the range of protocols that can be analysed using this approach, we have applied our equivalence checking tool to specify and verify interesting and practical quantum protocols from teleportation to secret sharing.
Geometrisation of First-Order Logic
Roy Dyckhoff
We show that every first-order theory T has a conservative extension G_T that is a geometric theory. Reasoning problems in T can therefore be replaced by problems in G_T, where the methods of geometric (aka ‘coherent’) logic are applicable. We discuss related work by Skolem (1920), Antonius (1975), Bezem and Coquand (2005), Fisher (2007–..), Polonsky (2011) and Mints (2012).
(A formula is **positive** iff built from atoms using \exists, \land and \lor. A **geometric implication** is the universal quantification of a formula C -> D where C and D are positive. A theory is **geometric** iff axiomatised by geometric implications. Lots of mathematical theories are geometric. Reasoning in a geometric theory usually avoids the unnatural conversions of resolution-based theorem proving, and produces intuitionistically sound proofs)
The Polygonal Jordan Curve Theorem without Ruler or Compass
Phil Scott
In this talk, I will recount my HOL Light verification of the Polygonal Jordan Curve Theorem. The verification is based on very simple axioms for ordered geometry, those which appear in Hilbert's seminal Foundations of Geometry. Hilbert gave no proof of the theorem, and there are few in the literature. My verification is adapted from Veblen's 1904 proof. But as I hope to convey, the details are much more subtle than the traditional proofs would imply, and the axiomatic system used presents some challenges for automated theorem proving.
On the Sato et al. map-skeleton representation of lambda terms
James McKinna
In recent work by Sato/Pollack/Schwichtenberg/Takafumi (in the de Bruijn memorial volume of the Indagationes), a canonical representation of name-carrying lambda terms is given, based on a novel datastructure for representing binding, the so-called "map/skeleton" representation.
Their paper leaves as future work the challenging problem of how to give an adequate representation of the important judgments of interest (reduction, typing, ...) one might wish to define on such terms.
I have proposed a modest (indeed: conservative) extension to their language which appears to solve this problem. I have formalised the proof of conservativity of the extension in Isabelle2013. Inter alia, the extension is based on a generalisation of Kleene's notion of "pure variable proof" (IMM, \S 78, p451), and the proof of conservativity on a modified version of McKinna-Pollack style reasoning (TLCA1993, JAR1999).
In this talk I'll (quickly) recap the map/skel representation, describe my extension of it, and sketch the proof of conservativity for typing and reduction for a presentation of simply-typed lambda calculus in the extended system.
This seminar was organised by Alice Miller and Yu Lu. For further information please contact: alice.miller@glasgow.ac.uk