Speaker / Predavač
José Carlos Espírito Santo, University of Minho, Braga, Portugal
Naslov / Title
The polarized lambda-calculus
Sažetak / Abstract
Abstract: A natural deduction system isomorphic to the focused sequent calculus for polarized intuitionistic logic is proposed. The system comes with a language of proof-terms, named polarized lambda-calculus, whose reduction rules express simultaneously a normalization procedure and the isomorphic copy of the cut-elimination procedure pertaining to the focused sequent calculus. Noteworthy features of this natural deduction system are: how the polarity of a connective determines the style of its elimination rule; the existence of a proof-search strategy which is equivalent to focusing in the sequent calculus; the highly-disciplined organization of the syntax - even atoms have introduction, elimination and normalization rules. The polarized lambda-calculus is a programming formalism close to call-by-push-value, but justified by its proof-theoretical pedigree.
vreme: utorak, 25.10.2016. u 16:00
mesto: sala 305 (Nastavni blok, FTN)