People

Research activity in 1995

L'attivita' di ricerca ha riguardato essenzialmente i punti seguenti:

• Studio dei lambda termini rappresentanti prove nei sistemi formali per la matematica costruttiva, e il loro uso per la sintesi automatica di programmi.


• Studio della nozione di tipo in sistemi fortemente tipati e suoi collegamenti con le nozioni di teorema e dimostrazione in logica.


• Studio della nozione di tipo nei linguaggi di programmazione e sistemi di tipi con proprieta' di ereditarieta' per modellare concetti di programmazione orientata ad oggetti.


• Studio delle strategie per l'inferenza automatica dei tipi, in sistemi con operatori non standard come l'intersezione e l'unione.


• Analisi delle principali proprieta' sintattiche e semantiche di alcuni sistemi di tipi polimorfi contenenti interessanti operatori per la formazione di tipi (come l'esponenziazione, la quantificazione universale ed esistenziale, l'intersezione, l'unione e la ricorsione).


• Studio del lambda-calcolo lineare e sua semantica categoriale.


• Semantica di varianti del lambda calcolo, che modella il comportamento dei linguaggi call-by-value, usando i tre approcci standard per esprimere la semantica dei linguaggi, cioe' l'approccio operazionale, denotazionale e logico.


• Caratterizzazioni di operatori proof-teoretici di tipi, che esprimono nozioni di dipendenze funzionali fra algoritmi, mediante la nozione di derivabilita' in logiche non classiche, come la logica della Rilevanza.

1995 Publications

F. Barbanera, M. Dezani-Ciancaglini, U. De' Liguoro, "Intersection and Union Types: Syntax and Semantics", Information and Computation , 119(2), 202-230, 1995.

F. Barbanera, M. Fernandez, "Intersection Type Assignment Systems with Algebraic Rewriting", Theoretical Computer Science, to appear.

S. Berardi, "Pruning Simply Typed Lambda-terms", Journal of Logic and Computation, to appear.

S. Berardi, M. Bezem, T. Coquand, "On the Computational Content of the Axiom of Choice", TLCA'95, LNCS 902, Springer Verlag, 47-62, 1995.

S. Berardi, L. Boerio, "Using Subtyping in Program Optimization", TLCA'95, LNCS 902, Springer Verlag, 63-77, 1995.

V. Bono, L. Liquori, "A Subtyping for the Fisher-Honsel-Mitchell Calculus of Objects", CSL '94 , LNCS 933, 16-30, 1995.

M. Coppo, P. Giannini, "Principal Types and Unification for a Simple Intersection System", Information and Computation, 122(1), 70-96, 1995.

L. Liquori, S. Van Bakel , S. Ronchi Della Rocca, P. Urzyczyn , "Comparing Cubes of Typed and Type Assignment Systems", Annals of Pure and Applied Logic, to appear.

I. Margaria, M. Zacchi, "Principal Typing in a Discipline", Journal of Logic and Computation, 5(3), 367-381, 1995.

A. Pravato, S. Ronchi Della Rocca, L. Roversi, "Categorical Semantics of call-by-value Lambda Calculus", TLCA '95, LNCS 902, 381-396, 1995.

S. Van Bakel, M. Fernandez, "Approximation and Normalization Results for Typeable Term Rewriting Systems", HOA '95, LNCS, Springer Verlag, to appear.

S. Van Bakel and M. Fernandez, "(Head-) Normalization of Typeable Rewrite Systems", RTA '95, LNCS 914, Springer-Verlag, 279-293, 1995.

S. Van Bakel, "Intersection Type Assignment Systems", Theoretical Computer Science , 151, 1995, to appear.

S. Van Bakel, "Rank2 Intersection Type Assignment in Term Rewriting Systems", Fundamenta Informaticae, 1995, to appear.