Linear two-sorted constructive arithmetic

Helmut Schwichtenberg - Universität München
Data e ora
martedì 15 marzo 2016 alle ore 16.00 - rinfresco 15.45, inizio seminario 16.00
Ca' Vignal - Piramide, Piano 0, Sala Verde
Peter Michael Schuster
Referente esterno
Data pubblicazione
1 febbraio 2016


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.

© 2002 - 2021  Università degli studi di Verona
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234