Progetto di ricerca di ateneo - 1999

Eugenio Moggi March 13, 1998

NOTA. Abbiamo indicato come ambito di ricerca per il progetto di ateneo il dipartimento. Tuttavia, il progetto ha notevoli sinergie con il progetto di interesse nazionale “Tecniche formali per la specifica, l’analisi, la verifica, la sintesi e la trasformazione di sistemi software”, che ha ottenuto il cofinanziamento MURST per gli anni 1998-99, e a cui partecipano molti dei ricercatori coinvolti nella presente proposta. Inoltre, e’ possibile che una parte del finanziamento che l’ateneo dara’ sia utilizzata per cofinanziare progetti nazionali in fase di allestimento (ed il cui inizio e’ previsto nel 1999), a cui dovrebbero partecipare alcuni dei ricercatori coinvolti nella presente proposta.

Area:  01
Disciplina: K05B
Titolo:  modelli, metodi, linguaggi per progettazione di software
Durata:  12 mesi (continuazione)
Resposabile: Moggi Eugenio

Professori e ricercatori universitari UniGe

1. E.Astesiano (PO)

2. M.Cerioli (RC)

3. G.Costa (PO)

4. M.Martelli (PO)

5. G.Reggio (PA)

6. E.Zucca (RC) Dottorandi e borsisti post dottorato UniGe

1. D.Ancona (BC)

2. G.Belle’ (DD)

3. E.Coscia (DD)

4. F.Zini (DD)

5. C.Calcagno (DD)

6. M.Bozzano (DD)

7. V.Mascardi (DD) Altri

1. Fabrizio Palumbo (AL, GE) laureando

2. Giorgio Delzanno (AL) collaboratore esterno

1999

attrezzature  15
materiale consumo  15
missioni  25

personale esterno

altre voci  15
totale A+B  70

Descrizione ed obbiettivi della ricerca

Cio’ che e’ riportato dopo la richiesta di input e’ la descrizione/obbiettivo indicato nella precedente proposta.

Descrizione ricerca: Il progetto si incentra sullo studio e sviluppo di costrutti ad alto livello nell’ambito dei paradigmi di programmazione (funzionale, logico e concorrente) e dei formalismi di specifica. In particolare si vuole valutare l’espressivita’ ed implementabilita’ dei construtti, e la congruita’ tra formalismi e metodi di specifica. La ricerca si articola in quattro filoni:

1. Studio di semantiche intensionali per modellare linguaggi a due livelli usati nell’ambito della ottimizzazione basata sulla tecnica della ”partial evaluation”, e utilizzo di tali semantiche per stabilire la correttezza della valutazione parziale.

2. Studio dell’applicazione dei linguaggi di programmazione logica lineare di ordine superiore per la modellizzazione di sistemi concorrenti ad oggetti e di sistemi multi-agente. Studio degli aspetti implementativi di un ambiente di prototipazione rapida per tali sistemi, attualmente in via di sperimentazione sulla base di una metodologia di sviluppo ad agenti.

Studio di estensioni alla Programmazione Logica basata su aspetti object e database-oriented. La metodologia seguita si basa sullo studio della Logica Lineare dal punto vista della teoria della dimostrazione dalla relazione tra dimostrazioni e computazioni.

3. Estensioni del linguaggio CASL per sistemi reattivi e studio di un metodo di sviluppo del software basato su CASL e/o sue estensioni. Progettazione di un metodo di specifica per programmi Java. Studio del concetto di feature per la definizione di un metodo di specifica per sistemi dinamici che supporti l’evoluzione.

4. Analisi dell’espressivita’ del linguaggio di moduli mixin precedentemente sviluppato tramite lo studio della traduzione in tale linguaggio di operatori ad alto livello presenti in linguaggi modulari reali. Definizione di regole di riduzione che permettano di semplificare espressioni di modulo complesse.

Obbiettivi primo esercizio finanziario:

1. Studio di un linguaggio a due livelli semplicemente tipato: semantica e correttezza.

2. Studio di un linguaggio logico lineare per la specifica di sistemi multi-agente.

3. Metodologie e formalismi per lo sviluppo di sistemi reattivi (estensioni di CASL e supporto per l’evoluzione).

4. Definizione di un calcolo di moduli mixin che soddisfi proprieta’ quali confluenza e normalizzazione.

Altri finanziamenti

Responsabile, Ente erogatore, Inizio, Fine, Spese attrezzature, Spese Ricerca

1. Moggi, CEC, Aprile 1998, Aprile 2001, — , 30 MITL

2. Moggi, MURST, Febbraio 1998, Febbraio 2000, 20 MITL , 95 MITL (cofinanziamento MURST)

[1] D. Ancona, E. Zucca. An algebraic approach to mixins and modularity. In M. Hanus and M. Rodríguez Artalejo, editors, ALP ’96 - 5th Intl. Conf. on Algebraic and Logic Programming, LNCS 1139, pages 179–193, Berlin, 1996. Springer Verlag.

[2] D. Ancona, E. Zucca. A formal framework for modules with state. In M. Wirsing and M. Nivat, editors, AMAST ’96 - Algebraic Methodology and Software Technology, LNCS 1101, pages 148–162, Berlin, 1996. Springer Verlag.

[3] E. Astesiano, G. Reggio. A Dynamic Specification of the RPC-Memory Problem. In M. Broy, S. Merz, and K. Spies, editors, Formal System Specification: 15 Contributions for the RPC-Memory Specification, LNCS 1169. Springer Verlag, Berlin, 1996.

[4] E. Astesiano, E. Zucca. A free construction of dynamic terms. Journ. of Computer and System Sciences, 52(1):143–156, February 1996.

[5] G. Belle’, B. Jay, E. Moggi. Functorial ML. In PLIPL ’96, LNCS 1140. Springer Verlag, 1996.

[6] E. Coscia, G. Reggio. Deontic Concepts in the Algebraic Specification of Dynamic Systems: The Permission Case. In M. Haveraaen, O. Owe, and O.-J. Dahl, editors, Recent Trends in Data Type Specification, LNCS 1130, pages 161–182. Springer Verlag, Berlin, 1996.

[7] E. Zucca. From static to dynamic abstract data-types. In W.Penczek and A. Szałas, editors, Mathematical Foundations of Computer Science 1996, LNCS 1113, pages 579–590, Berlin, 1996.

[8] E. Astesiano, G. Reggio. Formalism and Method in M. Bidoit, M. Dauchet editors Proc. TAPSOFT ’97 LNCS 1214, 93–114, Springer Verlag, 1997.

[9] M. Cerioli, J. Meseguer. May I borrow your logic? (transporting logical structures along maps). Theoretical Computer Science, 173(2):311–347, 1997.

[10] M. Cerioli, A. Haxthausen, B. Krieg-Bruckner, T. Mossakowski. Permissive subsorted partial logic in CASL. in Proceedings AMAST’97, LNCS 1349, 1997.

[11] G. Costa, G. Reggio. Specification of Abstract Dynamic Data Types: A Temporal Logic Approach Theoretical Computer Science, 173 (2) :513–554, 1997.

[12] E. Bertino, M. Martelli, D. Montesi. Transactions and Updates in Deductive Databases. IEEE Transactions on Knowledge and Data Engineering Vol. 9, N. 5, pp.784-797, 1997.

[13] M. Bozzano, G. Delzanno, M. Martelli. A Linear Logic Semantics for Object-Oriented, Deductive and Active Databases In Proceedings of APPIA-GULP-PRODE ’97, pages 105-115, Grado, Italy, 1997.

[14] M. Bozzano, G. Delzanno, M. Martelli. A Linear Logic Specification for Chimera”. In Proceedings of ILPS’97 Post-Conference Workshop DYNAMICS’97 on Transactions and Change in Logic Programming and Deductive Databases, Port Jefferson, New York, USA, 1997.

[15] M. Martelli, V. Mascardi, F. Zini. CaseLP: a Complex Application Specification Environment based on Logic Programming. In Proceedings of ICLP’97 Post Conference Workshop on Logic Programming and Multi-Agents, pages 35-50, Leuven, Belgium, July 1997.

[16] M. Martelli, V. Mascardi, F. Zini. Applying Logic Programming to the Specification of Complex Applications (extended version). In Proceedings of APPIA-GULP-PRODE ’97, pages 491-499, Grado, Italy, June 1997.

[17] M. Martelli, V. Mascardi, F. Zini. Applying Logic Programming to the Specification of Complex Applications. In Mathematical Modelling and Scientific Computing, vol.8, September 1997.

[18] G. Belle’, E. Moggi. Typed intermediate languages for shape analysis. In TLCA ’97 LNCS 1210, Springer Verlag, 1997.

[19] E. Moggi. A categorical account of two-level languages. In MFPS XIII, ENTCS. Elsevier, 1997.

[20] D.Ancona, E. Zucca. Overriding operators in a mixin-based framework in H. Glaser, P. Hartel and H. Kuchen editors Proc. PLILP’97, LNCS 1292, 47–61, Springer Verlag, 1997.

Allegato 4 - lista pubblicazioni 1994-97

Area:  01
Disciplina: K05B
Titolo:  modelli, metodi, linguaggi per progettazione di software
Resposabile: Moggi Eugenio

[1] F. Alessi, P. Baldan, G. Bellè. A fixed-point theorem in a category of compact metric spaces. Theoretical Computer Science, 146:311–320, 1995.

[2] D. Ancona, E. Zucca. An algebraic approach to mixins and modularity. In M. Hanus and M. Rodríguez Artalejo, editors, ALP ’96 - 5th Intl. Conf. on Algebraic and Logic Programming, number 1139 in Lecture Notes in Computer Science, pages 179–193, Berlin, 1996. Springer Verlag.

[3] D. Ancona, E. Zucca. A formal framework for modules with state. In M. Wirsing and M. Nivat, editors, AMAST ’96 - Algebraic Methodology and Software Technology, number 1101 in Lecture Notes in Computer Science, pages 148–162, Berlin, 1996. Springer Verlag.

[4] E. Astesiano, E. Battiston, F. De Cindio, R. De Nicola, S. Gnesi, A. Maggiolo Schettini, G. Reggio. Metodologie e Strumenti per la Specifica e la Verifica di Sistemi Concorrenti. In G. Filè, editor, Ambienti per Linguaggi di Nuova Concezione. Franco Angeli, 1995.

[5] E. Astesiano, F. Morando, G. Reggio. The SMoLCS Toolset. In P.D. Mosses, M. Nielsen, and M.I. Schwartzbach, editors, Proc. of TAPSOFT ’95, number 915 in Lecture Notes in Computer Science, pages 810–811. Springer Verlag, Berlin, 1995.

[6] E. Astesiano, G. Reggio. A Dynamic Specification of the RPC-Memory Problem. In M. Broy, S. Merz, and K. Spies, editors, Formal System Specification: 15 Contributions for the RPC-Memory Specification, LNCS 1169. Springer Verlag, Berlin, 1996.

[7] E. Astesiano, E. Zucca. D-oids: a model for dynamic data-types. Mathematical Structures in Computer Science, 5(2):257–282, June 1995.

[8] E. Astesiano, E. Zucca. A free construction of dynamic terms. Journ. of Computer and System Sciences, 52(1):143–156, February 1996.

[9] G. Belle’, B. Jay, E. Moggi. Functorial ML. In PLIPL ’96, LNCS 1140. Springer Verlag, 1996.

[10] A. Bossi, M. Gabbrielli, G. Levi, M. Martelli, “The s-semantics approach: theory and applications”. Journal of Logic Programming, 19,20: 149-197, 1994.

[11] R. Breu, E. Zucca. An algebraic semantic framework for object oriented languages with concurrency (extended abstract). Formal Aspects of Computing, 8(6):706–715, 1996.

[12] M. Bugliesi, G. Delzanno, L. Liquori, M. Martelli. “A Linear Logic Calculus of Objects”. In Proceedings of Int. Conf. and Symp. Logic Programming, pages 67–81, The MIT Press, Bonn, 1996.

[13] M. Cerioli, G. Reggio. Algebraic-oriented institutions. In T. Rus M. Nivat, C. Rattray, G. Scollo, editors, Algebraic Methodology and Software Technology 1993, Workshops in Computing, 103–210. Springer Verlag, Berlin, 1994.

[14] E. Coscia, G. Reggio. Deontic Concepts in the Algebraic Specification of Dynamic Systems: The Permission Case. In M. Haveraaen, O. Owe, and O.-J. Dahl, editors, Recent Trends in Data Type Specification, number 1130 in Lecture Notes in Computer Science, pages 161–182. Springer Verlag, Berlin, 1996. 11th Workshop on Specification of Abstract Data Types joint with the 8th general COMPASS workshop. Oslo, Norway, September 1995. Selected papers.

[15] A. Di Pierro, M. Martelli, C. Palamidessi. “Negation as Instantiation”. Information and Computation, 120, 2, pp. 263-278, 1995.

[16] G. Delzanno, M. Martelli. “Objects in Forum”. In Proceedings of The International Logic Programming Symposium, pages 115–129, The MIT Press, 1995.

[17] G. Delzanno, M. Martelli. “Forum & Objects”. In Proc. GULP-PRODE’95, Vietri, 1995.

5

[18] G. Delzanno, M. Martelli. “Proofs as Computations in Linear Logic”. In Proc. APPIA-GULP-PRODE’96, pp. 155-166, San Sebastian, 1996.

[19] M. Fiore, E. Moggi, D Sangiorgi. A fully-abstract model for the pi-calculus. In 11th LICS Conference. IEEE, 1996.

[20] A. Giordana, L. Saitta, F. Zini. Learning disjunctive concepts by means of genetic algorithms. In Proc. 11th International Conference on Machine Learning, pages 96–104, New Brunswick, New Jersey, 1994.

[21] J.M.E. Hyland, E. Moggi. The S-replete construction. In CTCS 1995, volume 953 of LNCS. Springer Verlag, 1995.

[22] M. Martelli, A. Messora, C. Palamidessi, A. H. Bon Hoa, “Fixpoint Semantics of L_{λ}”, Proc. GULP-PRODE’94, Peniscola (Spain), 1994.

[23] E. Moggi. A general semantics for evaluation logic. In 9th LICS Conf. IEEE, 1994.

[24] E. Moggi. A semantics for evaluation logic. Fundamenta Informaticae, 22(1/2), 1995.

[25] M. Bettaz, G. Reggio. AA SMoLCS Based Kit for Defining the Semantics of High-Level Algebraic Petri Nets. In H. Ehrig and F. Orejas, editors, Recent Trends in Data Type Specification, number 785 in Lecture Notes in Computer Science. Springer Verlag, Berlin, 1994.

[26] E. Zucca. Implementation of data structures in an imperative framework. In Recent Trends in Data Type Specification (10th Workshop on Specification of Abstract Data Types joint with the 5th COMPASS Workshop - Selected Papers), number 906 in Lecture Notes in Computer Science, pages 483–498. Springer Verlag, Berlin, 1995.

[27] E. Zucca. From static to dynamic abstract data-types. In W.Penczek and A. Szałas, editors, Mathematical Foundations of Computer Science 1996, number 1113 in Lecture Notes in Computer Science, pages 579–590, Berlin, 1996. Springer Verlag.

[28] E. Astesiano, G. Reggio. Formalism and Method in M. Bidoit, M. Dauchet editors Proc. TAPSOFT ’97 LNCS 1214, 93–114, Springer Verlag, 1997.

[29] M. Cerioli, J. Meseguer. May I borrow your logic? (transporting logical structures along maps). Theoretical Computer Science, 173(2):311–347, 1997.

[30] M. Cerioli, A. Haxthausen, B. Krieg-Bruckner, T. Mossakowski. Permissive subsorted partial logic in CASL. in Proceedings AMAST’97, LNCS 1349, 1997.

[31] G. Costa, G. Reggio. Specification of Abstract Dynamic Data Types: A Temporal Logic Approach Theoretical Computer Science, 173 (2) :513–554, 1997.

[32] G. Reggio, M. Larosa. A Graphic Notation for Formal Specifications of Dynamic Systems in J. Fitzgerald, C.B. Jones editors Proc. FME 97 - Industrial Applications and Strengthened Foundations of Formal Methods LNCS 1313, 93–114, Springer Verlag,1997.

[33] E. Bertino, M. Martelli, D. Montesi. Transactions and Updates in Deductive Databases. IEEE Transactions on Knowledge and Data Engineering Vol. 9, N. 5, pp.784-797, 1997.

[34] G. Delzanno. Logic and Object-Oriented Programming in Linear Logic. Thesis for the PhD Dissertation, Department of Computer Science, University of Pisa, March 1997.

[35] M. Bozzano, G. Delzanno, M. Martelli. A Linear Logic Semantics for Object-Oriented, Deductive and Active Databases. In Proceedings of APPIA-GULP-PRODE ’97, Grado, Italy, 1997.

[36] M. Bozzano, G. Delzanno, M. Martelli. A Linear Logic Specification for Chimera. In Proceedings of ILPS’97 Post-Conference Workshop DYNAMICS’97 on Transactions and Change in Logic Programming and Deductive Databases, Port Jefferson, New York, USA, 1997.

[37] M. Martelli, V. Mascardi, F. Zini. CaseLP: a Complex Application Specification Environment based on Logic Programming. In Proceedings of ICLP’97 Post Conference Workshop on Logic Programming and Multi-Agents, pages 35-50, Leuven, Belgium, July 1997.

[38] M. Martelli, V. Mascardi, F. Zini. Applying Logic Programming to the Specification of Complex Applications (extended version). In Proceedings of APPIA-GULP-PRODE ’97, pages 491-499, Grado, Italy, June 1997.

[39] M. Martelli, V. Mascardi, F. Zini. Applying Logic Programming to the Specification of Complex Applications. In Mathematical Modelling and Scientific Computing, vol.8, September 1997.

[40] G. Belle’, E. Moggi. Typed intermediate languages for shape analysis. In TLCA ’97 LNCS 1210, Springer Verlag, 1997.

[41] E. Moggi. Metalanguages and applications. In Semantics and Logics of Computation Publications of the Newton Institute, Cambridge University Press, 1997.

[42] E. Moggi. A categorical account of two-level languages. In MFPS XIII, ENTCS. Elsevier, 1997.

[43] D.Ancona, E. Zucca. Overriding operators in a mixin-based framework in H. Glaser, P. Hartel and H. Kuchen editors Proc. PLILP’97 9th Int. Symp. on Programming Languages, Logics and Programs LNCS 1292, 47–61, Springer Verlag, 1997.

[44] D. Ancona, E. Zucca. An Algebra of Mixin Modules, WADT’97 (12th Workshop on Algebraic Development Techniques - Selected Papers). LNCS to appear, Berlin, Springer Verlag.