Pure and Applied Logic Colloquium October 25, 2018 4:30pm — 5:45pm Location: Steinberg Auditorium A53 - Baker Hall Speaker: LIRON COHEN, Postdoctoral Associate, Cornell University - https://www.cs.cornell.edu/%7Elironcohen/ Enhancing the Proofs-as-Programs Paradigm with Modern Notions of Computation and Reasoning Techniques Speaker: Liron Cohen Location: Baker Hall Steinberg Auditorium A53 Enhancing the Proofs-as-Programs Paradigm with Modern Notions of Computation and Reasoning Techniques The proofs-as-programs paradigm which establishes a correspondence between formal proofs and computer programs has made tremendous impact on the world of computing, enabling various high-value applications in different areas of computer science. However, while both proof theory and programming languages have evolved significantly over the past years, the cross-fertilization of the independent new developments in each of these fields has yet to be explored in the context of the paradigm. This naturally gives rise to the following questions: how can modern notions of computation influence and contribute to formal foundations, and how can modern reasoning techniques improve the way we design and reason about programs? In this talk we focus on the first question and demonstrate how by using programming principles that go beyond the standard lambda-calculus, namely state and non-determinism, it is possible to provide new insights into foundational mathematical concepts, namely free choice sequences and the Axiom of Choice. Event Website: https://www.cmu.edu/dietrich/philosophy/events/lectures-colloquia/ For More Information: mjoseph@andrew.cmu.edu
