Research activity in 1996
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.
1996 Publications
S. Van Bakel, F. Barbanera, M. Fernandez, Approximation and
Normalization Results for Typable Term Rewriting Systems with Beta Rule,
ESOP'96 , LNCS 1058, 387-403, 1996.
F. Barbanera, S. Berardi, Proof-irrelevance out of Excluded-middle and Choice
in the Calculus of Constructions, Journal of Functional Programming ,
vol.6(3), 519-525, 1996.
F. Barbanera, S. Berardi, A Symmetric Lambda-Calculus for ``Classical'' Program
Extraction, Information and Computation , vol.125, No.2, 103-117,
1996.
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.
V.Bono, M.Bugliesi, M.Dezani, and L.Liquori, Subtyping Constraints for
Incomplete Objects, CAAP'97 , LNCS, to appear.
V.Bono, M.Bugliesi, Matching Constraints for the Lambda Calculus of Objects,
TLCA'97, LNCS, to appear.
V. Bono, M. Bugliesi, L. Liquori, A Lambda Calculus of Incomplete Objects,
MFCS'96 , LNCS 1113, 218-229, 1996.
M. Bugliesi, G.Delzanno, L. Liquori, and M. Martelli, A Linear Logic Calculus
of Objects,JICSLP'96, 79--94, The MIT Press, 1996.
M.Coppo, S. Berardi (editors) Types for Proofs and Programs :TYPES '95
, LNCS 1158, 1996.
M. Coppo, F. Damiani, P. Giannini, Refinement Types for Program Analysis,
SAS'96 LNCS 1145, 143-158, 1996.
F. Damiani, P. Giannini, An Algorithm Inference for Strictness, TLCA'97 ,
LNCS, to appear.
M.Dezani-Ciancaglini, de' Liguoro, U. and A.Piperno, Filter Models for
Conjunctive-Disjunctive Lambda-Calculi, Theoretical Computer Science
170(1-2), 1996, 83-128.
M.Dezani-Ciancaglini, de' Liguoro, U. and A.Piperno, A Filter Model for
Concurent Lambda-Calculus, SIAM Journal on Computing , to appear.
M.Dezani-Ciancaglini, B.Venneri, The "Relevance" of Intersection and Union
Types, Notre Dame Journal of Formal Logic , to appear.
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.
L. Liquori, and B. Castagna, A Typed Lambda Calculus of Objects,
ASIAN-96 , LNCS 1212, 129--141, 1996.
