University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Towards a geometry for syntax

Towards a geometry for syntax

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

  • UserJon Sterling, University of Aarhus
  • ClockFriday 19 November 2021, 14:00-15:00
  • HouseSS03.

If you have a question about this talk, please contact Jamie Vicary.

The purpose of this talk is to pose the question, “What are the Euclid’s postulates for syntactic metatheory?”

In the fourth century B.C.E., the Greek mathematician Euclid set down his famous postulates for plane geometry, explaining geometric shapes in terms of rules that govern their construction and incidence. The dialectical relationship between theories (axioms) and their models (coordinate systems) has been the driving force in the last two millennia of geometrical investigation.

In logic and computer science, workers in the “syntactic metatheory” investigate questions that lie on the fringe between a theory and its models — definability, normalization, decidability, conservativity, computational adequacy, parametricity, type safety, etc. Dominant methods attack these questions by means of explicit computations (e.g. Kripke logical relations) which practitioners have found to be both reliable and somewhat opaque. In this talk, I introduce Synthetic Tait computability — a new system of axioms that transforms these explicit computations into synthetic manipulations; classical Kripke logical relations can be seen as models or “coordinate systems” for the new geometry of syntax that is beginning to unfold.

Synthetic Tait computability has already been employed to positively resolve the normalization and decidability conjectures for cubical type theory, as well as a number of other recent results.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

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