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

## Interpreters for FreeAdd to your list(s) Download to your calendar using vCal - Philip Wadler (University of Edinburgh)
- Friday 08 July 2022, 13:30-14:30
- Seminar Room 1, Newton Institute.
If you have a question about this talk, please contact nobody. VS2W01 - Vistas in Verified Software In a proof assistant based on intuitionistic logic, a standard proof of type soundness automatically yields an interpreter for the corresponding language. This fact is obvious in retrospect, but there is evidence it was not obvious in prospect. The talk describes applications in the textbook Programming Language Foundations in Agda and to the Cardano blockchain. In connection with the latter, we explain why and how Reynolds’s and Girard’s System F, from the 1970s, is used to encode smart contracts that manipulate billions of dollars worth of assets: if you want a system that will still be running in fifty years, use one that is fifty years old! This talk is part of the Isaac Newton Institute Seminar Series series. ## This talk is included in these lists:- All CMS events
- Featured lists
- INI info aggregator
- Isaac Newton Institute Seminar Series
- School of Physical Sciences
- Seminar Room 1, Newton Institute
- bld31
Note that ex-directory lists are not shown. |
## Other listsCambridge Statistics Discussion Group (CSDG) Fluid Mechanics (DAMTP) DAMTP Jubilee Celebration## Other talksTea and Coffee Break The implicit boundary integral method BSU Seminar: “Optimising the discovery and development of gene silencing drugs with genetics and genomics” Modularity of Calabi-Yau Varieties Height pairings for algebraic cycles. Biextensions, generalized cross-ratios, Tamagawa numbers, and the Birch and Swinnerton Dyer conjecture |