Intesection types and resource control in the intuitionistic sequent lambda calculus

Abstract

This thesis studies computational interpretations of the intuitionistic sequent calculus with implicit and explicit structural rules, with focus on the systems with intersection types. The contributions of the thesis are grouped into three parts. In the first part intersection types are introduced into the lambda Gentzen calculus. The second part presents an extension of the lambda Gentzen calculus to a term calculus with resource control, i.e. with explicit operators for contraction and weakening, and apropriate intersection type assignment system which characterises strong normalisation in the proposed calculus. In the third part both previously studied calculi are integrated into one framework by introducing the notion of the resource control cube.

Ова дисертација се бави рачунским интерпретацијама интуиционистичког секвентног рачуна са имплицитним и експлицитним структурним правилима, са фокусом на типске системе са пресеком. Оригинални резултати тезе су груписани у три целине. У првом делу су типови са пресеком уведени у lambda Gentzen рачун. Други део представља проширење lambda Gentzen рачуна на формални рачун са контролом ресурса, тј. са експлицитним операторима контракције и слабљења, као и одговарајући типски систем са пресеком који карактерише јаку нормализацију у уведеном рачуну. У трећем делу оба рачуна су интегрисана у заједнички оквир увођењем структуре resource control cube.

Ova disertacija se bavi računskim interpretacijama intuicionističkog sekventnog računa sa implicitnim i eksplicitnim strukturnim pravilima, sa fokusom na tipske sisteme sa presekom. Originalni rezultati teze su grupisani u tri celine. U prvom delu su tipovi sa presekom uvedeni u lambda Gentzen račun. Drugi deo predstavlja proširenje lambda Gentzen računa na formalni račun sa kontrolom resursa, tj. sa eksplicitnim operatorima kontrakcije i slabljenja, kao i odgovarajući tipski sistem sa presekom koji karakteriše jaku normalizaciju u uvedenom računu. U trećem delu oba računa su integrisana u zajednički okvir uvođenjem strukture resource control cube.