Pure and Applied Logic Colloquium
— 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