Events

Date: 1 November 2024   Time: 15:00 - 17:00

Location: Peter Landin 4.24

A sequence of introductory talks:

Soren Riis: "Deduction-Preserving Recursive Isomorphisms Between Theories: A Hidden Gem from Pour-El & Kripke (1966)"

In a short four-page paper from 1966, Pour-El and Kripke published a striking yet surprisingly unknown result that appears to defy intuition. We tend to perceive fundamental axiom systems like Zermelo-Fraenkel set theory (ZFC) and Peano Arithmetic (PA) as very different mathematical theories, but from a certain perspective, all strong axiom systems are isomorphic. This result extends Myhill's isomorphism theorem: where Myhill showed that recursively enumerable sets that are mutually 1-1 reducible must be recursively isomorphic. Pour-El and Kripke proved that theories like PA and ZFC are "recursively isomorphic". Specifically, there exists a computable bijection f between statements of PA and ZFC that maps theorems to theorems, refutable statements to refutable statements, and independent statements to independent statements, while preserving much of the underlying deductive structure.

Nikos Tzevelekos: I will talk about reachability in pushdown systems (a pushdown system is
a pushdown automaton in which the input alphabet is not relevant/used).
It is known that if we look at pushdown automata as systems that use a
stack to evolve and can reach certain configurations, their reachability
problem becomes tractable for finite-state machines. I will describe one
so-called "saturation" technique to produce a finite-state machine from
a pushdown system and then show a novel (we think) technique to produce
this on the fly. This approach stems from a recent paper introducing a
novel technique for checking equivalence of stateful higher-order
programs [dl.acm.org/doi/10.1145/3661814.3662103].

The seminar will be followed by a social event at which all are welcome.