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)


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.



Agata Ciabattoni

Dale Miller, Inria Saclay – Île-de-France and the Laboratoire d’Informatique (LIX), UMR

Comments are closed.