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) > Bidirectional typing is not just an implementation technique

## Bidirectional typing is not just an implementation techniqueAdd to your list(s) Download to your calendar using vCal - Meven Lennon-Bertrand, University of Cambridge
- Friday 03 February 2023, 14:00-15:00
- SS03, Computer Laboratory.
If you have a question about this talk, please contact Jamie Vicary. In 2000, Pierce and Turner introduced a new technique to perform type inference for ML-like languages, whose main idea was to carefully understand the local flow of information in typing rules. This technique, which came to be referred to as bidirectional typing, did not come out of a void: similar ideas had appeared independently in other contexts. In particular, bidirectional typing has been a part of the folklore of dependently typed languages implementers since the dawn of time. But even in that context where it has a long history, bidirectional typing was missing an understanding that would detach from implementations to focus on the type-theoretic structure. Fortunately, such a type-theoretic bidirectional structure turns out to be a very interesting tool when studying (dependent) type systems. In my talk, I will try and give some of my understanding of bidirectional typing, how it is both rooted in type-checker implementations but is more than just this, and how it can be used to make the infamously painful meta-theory of dependent type systems a bit less painful. 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
- Computing and Mathematics
- Department of Computer Science and Technology talks and seminars
- Interested Talks
- Logic and Semantics Seminar (Computer Laboratory)
- SS03, Computer Laboratory
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsFaith in the Special Relationship: Strategic Implications of US-UK Alignment—and Divergence—on Religion Department of Public Health and Primary Care eSCAMPS 2020## Other talksHuman perception of transient longitudinal vehicle motion Discrete Helmholtz equation and the interaction of two perpendicular semi-infinite boundaries: one equation with tree unknown functions. LMB Seminar: Talking to cells: biomolecular ultrasound for imaging and control of cellular function in intact organisms 'The History and Politics of Capital Markets in Post-independence Africa: Comparative Insights from Nigeria and Kenya’ The Origins of Human Cooperation Research in the Goldman group: pandemic-scale phylogenetics, and optimizing new sequencing technologies |