COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

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

## Towards a geometry for syntaxAdd to your list(s) Download to your calendar using vCal - Jon Sterling, University of Aarhus
- Friday 19 November 2021, 14:00-15:00
- SS03.
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 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. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Cambridge talks
- Computer Laboratory talks
- Computing and Mathematics
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- SS03
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsFestival of Ideas: Spotlight Talks Polis Cambridge University United Nations Association## Other talksPast ice sheet evolution: West Antarctica during warm climate intervals Food as Expression Title: An outbreak of heart failure at Moe’s Tavern How are red and blue quasars different? CorrosionRADAR - A journey from an invention to a global corrosion monitoring company Ethics for the working mathematician, discussion 8: Looking into the future, what more can mathematicians do? |