Dale Miller
Separating Functional Computation from Relations
Theory and Logic Group, and VCLA hosted a talk by Dale Miller
| DATE: | Wednesday, October 31, 2018 |
| TIME: | 16:30 s.t. |
| VENUE: | Seminar Room Gödel, Favoritenstrasse 9-11, Ground Floor, (HB EG 10) |
ABSTRACT
The logical foundations of arithmetic generally start with a quantificational logic of relations. Of course, one often wishes to have a formal treatment of functions within this setting. Both Hilbert and Church used choice operators (such as the epsilon
operator) in order to coerce relations that happen to encode functions into actual functions. Others have extended the term language with confluent term rewriting in order to encode functional computation as rewriting to a normal form. We take a different approach that neither extends uses choice principles nor an equality theory. Instead, we use the familiar two-phase construction of focused proofs and capture functional computation entirely within one of these phases. As a result, our logic remains purely relational even when it is computing functions.
Joint work with Ulysse Gerard that was presented at CSL 2017.
CONTACT
Agata Ciabattoni
Dale Miller, Inria Saclay – Île-de-France and the Laboratoire d’Informatique (LIX), UMR
