BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Towards a geometry for syntax - Jon Sterling\, University of Aarhu
 s
DTSTART:20211119T140000Z
DTEND:20211119T150000Z
UID:TALK166285@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:The purpose of this talk is to pose the question\, “What are
  the Euclid’s postulates for syntactic metatheory?”\n\nIn the fourth c
 entury B.C.E.\, the Greek mathematician Euclid set down his famous postula
 tes for plane geometry\, explaining geometric shapes in terms of rules tha
 t govern their construction and incidence. The dialectical relationship be
 tween theories (axioms) and their models (coordinate systems) has been the
  driving force in the last two millennia of geometrical investigation.\n\n
 In logic and computer science\, workers in the “syntactic metatheory” 
 investigate questions that lie on the fringe between a theory and its mode
 ls — definability\, normalization\, decidability\, conservativity\, comp
 utational adequacy\, parametricity\, type safety\, etc. Dominant methods a
 ttack these questions by means of explicit computations (e.g. Kripke logic
 al relations) which practitioners have found to be both reliable and somew
 hat opaque. In this talk\, I introduce *Synthetic Tait computability* — 
 a new system of axioms that transforms these explicit computations into sy
 nthetic manipulations\; classical Kripke logical relations can be seen as 
 models or “coordinate systems” for the new geometry of syntax that is 
 beginning to unfold.\n\nSynthetic Tait computability has already been empl
 oyed to positively resolve the normalization and decidability conjectures 
 for cubical type theory\, as well as a number of other recent results.
LOCATION:SS03
END:VEVENT
END:VCALENDAR