Linear two-sorted constructive arithmetic

Relatore:  Helmut Schwichtenberg - Universität München
  martedì 15 marzo 2016 alle ore 16.00 rinfresco 15.45, inizio seminario 16.00
We consider a term system in the style of Gödel's system T together
with a computation model that allows to faithfully represent
polynomial-time algorithms.  To this end we follow a tradition initiated
by Simmons (1988) and developed by Bellantoni and Cook (1992), where two
sorts of variables are admitted, here called output and input variables.
The idea is that input variables are the general ones which may be
recursed on and used many times, whereas output variables cannot be
recursed on and can be used only once.  These ideas have been extended
to a higher type setting and hence -- via the Curry-Howard
correspondence -- to a linear two-sorted arithmetical system in the
style of Heyting arithmetic in all finite types.  Here we further extend
this setup with the aim to also include certain nonlinear algorithms
(like treesort), given by constants defined by equations involving
multiple recursive calls.

Luogo
Ca' Vignal - Piramide, Piano 0, Sala Verde

Referente
Peter Michael Schuster

Referente esterno
Data pubblicazione
1 febbraio 2016

Offerta formativa

Condividi