Progetto di ricerca di ateneo - 1997-98

Eugenio Moggi February 4, 1997

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

Professori e ricercatori universitari UniGe

1. E.Astesiano (PO)

2. M.Cerioli (RC)

3. G.Costa (PO)

4. S.Etalle (RL)

5. M.Martelli (PO)

6. C.Palamidessi (PO)

7. G.Reggio (PA)

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

1. D.Ancona (DD)

2. D.Archieri (DD)

3. G.Belle’ (DD)

4. E.Coscia (DD)

5. G.Delzanno (DD)

6. F.Zini (DD)

7. C.Calcagno (DD) Altri

1. Viviana Mascardi (AL, GE) laureata

2. Marco Bozzano (AL, GE) laureando

3. Massimo Schenone (AL, GE) laureando

1997 1998
attrezzature  20  30
materiale consumo  10  15
missioni  20  25

personale esterno

altre voci  20  20
totale A+B  70  90

Descrizione ed obbiettivi della ricerca

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 cinque filoni, che si estendono sui due esercizi finanziari:

1. Studio di semantiche intensionali per modellare una varieta’ di aspetti (p.e. la distinzione di fase), che saranno poi utilizzate per lo sviluppo di linguaggi intermedi a due livelli e di tecniche di analisi statica (p.e. dei costi di computazione).

2. 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. Studio di meccanismi di comunicazione e sincronizzazione per la programmazione concorrente e distribuita, con particolare attenzione agli aspetti innovativi introdotti dal pi-calcolo, dal join-calcolo, e dal ccp (concurrent constraint programming).

4. Studio delle mutue relazioni tra formalismi e metodi di specifica, tale ricerca e’ effettuata nel contesto della iniziativa COFI (Common Algebraic Framework Initiative), per lo sviluppo di un linguaggio di specifica algebrico comune.

5. Studio di un modello algebrico per i moduli mixin (moduli con componenti deferred), che sara’ poi utilizzato per proporre dei costrutti linguistici e delle regole di trasformazione per i moduli.

Obbiettivi primo esercizio finanziario: Definizione di linguaggi a due livelli per la shape-analysis. Sviluppo di un ambiente di programmazione logico e object-oriented , e studio di applicazioni databaseoriented. Analisi dell’espressivita’ e dell’implementabilita’ su architettura distribuita del pi-calcolo e di alcuni suoi frammenti. Definizione del linguaggio di base minimale per COFI, ed analisi degli attuali linguaggi di specifica per sistemi dinamici. Definizione di un linguaggio kernel per moduli mixin.

Obbiettivi secondo esercizio finanziario: Tecniche di analisi statica degli errori di shape e della complessita’. Studio di aspetti di concorrenza nel formalismo Ehhf per definire un linguaggio logico ad oggetti concorrente. Sviluppo di una versione distribuita del paradigma ccp in grado di supportare mobilita’ e cooperazione di agenti. Sviluppo di un metodo di specifica formale logico-algebrico per sistemi dinamici. Studio di leggi algebriche per il linguaggio dei moduli mixin.

Altri finanziamenti

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

1. Palamidessi, CEC, Gennaio 94, Dicembre 97, 12MITL, 78.5 MITL

2. Martelli, CNR, Agosto 96, Agosto 98, — , 20 MITL

3. Martelli, CNR, Ottobre 96, Ottobre 98, — , 10 MITL

4. Astesiano, CNR, Giugno 96, Giugno 98, — , 10 MITL

Attrezzature disponibili

1. ????

[1] D. Ancona and 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, Berlin, 1996.

[2] E. Astesiano, F. Morando, and 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.

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

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

[6] E. Best and C. Palamidessi Linear Constraint Systems as High-level Nets. In U. Montanari and V. Sassone, editors, Proc. of CONCUR 96, volume 1119 of Lecture Notes in Computer Science, pages 498–513. Springer-Verlag, 1996.

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

[8] 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.

[9] E. Coscia and 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 LNCS, pages 161–182. Springer Verlag, Berlin, 1996.

[10] F.S. de Boer, M. Gabbrielli, and C. Palamidessi. Proving Correctness of Constraint Logic Programs with Dynamic Scheduling. In R. Cousot and D.A. Schmidt, editors, Proc. of the Static Analysis Symposium (SAS 96), volume 1145 of Lecture Notes in Computer Science, pages 83–97. Springer-Verlag, 1996.

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

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

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

[14] S. Etalle. Unification-free prolog programs revisited. Journal of Programming Languages, (4), 1996.

[15] S. Etalle and M. Gabbrielli. Transformations of CLP modules. TCS, 166(1):101–146, 1996.

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

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

[18] R. McDowell, D. Miller, and C. Palamidessi. Encoding Transition Systems in Sequent Calculus: Preliminary Report Proc. of the Linear Logic Workshop, Tokyo, 29 March–2 April 1996.

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

[20] 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.

Allegato 4 - lista pubblicazioni 1993-96

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

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

[2] D. Ancona and 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 and 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] K. R. Apt and S. Etalle. On the unification free Prolog programs. In A. Borzyszkowski and S. Sokolowski, editors, Proceedings of the Conference on Mathematical Foundations of Computer Science (MFCS 93), Lecture Notes in Computer Science, pages 1–19, Berlin, 1993. Springer-Verlag.

[5] K.R. Apt, E. Marchiori, and C. Palamidessi. A Declarative Approach for First-Order Built-in’s of Prolog. Applicable Algebra in Engeneering, Communication and Computation 5(3/4):159–191, 1994.

[6] E. Astesiano, E. Battiston, F. De Cindio, R. De Nicola, S. Gnesi, A. Maggiolo Schettini, and 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.

[7] E. Astesiano, M. Cerioli. Relationships between logical frames. In Recent Trends in Data Type Specification, Lecture Notes in Computer Science 655, 126–143. Springer Verlag, Berlin, 1993.

[8] E. Astesiano, F. Morando, and 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.

[9] E. Astesiano, G. Reggio. A metalanguage for the formal requirement specification of reactive systems. In J.C.P. Woodcock, P.G. Larsen, editors, Proc. FME’93: Industrial-Strength Formal Methods, Lecture Notes in Computer Science 670. Springer Verlag, Berlin, 1993.

[10] E. Astesiano, G. Reggio. Specifying reactive systems by abstract events. In Proc. of Seventh International Workshop on Software Specification and Design. IEEE Computer Society, Los Alamitos, CA, 1993.

[11] E. Astesiano and 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.

[12] E. Astesiano, G. Reggio, E.Zucca. Stores as homomorphisms and their transformations. In A. M. Borzyszkowsky, S. Sokołowsky, editors, Proc. Mathematical Foundations of Computer Science 1993, Lecture Notes in Computer Science 611, 242–251. Springer Verlag, Berlin, 1993.

[13] E. Astesiano, E. Zucca. A semantic model for dynamic systems. In U.W. Lipeck, B. Thalheim, editors, Modelling Database Dynamics, Volkse 1992, Workshops in Computing, 63–83. Springer Verlag, Berlin, 1993.

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

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

6

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

[17] E. Best and C. Palamidessi Linear Constraint Systems as High-level Nets. In U. Montanari and V. Sassone, editors, Proc. of CONCUR 96, volume 1119 of Lecture Notes in Computer Science, pages 498–513. Springer-Verlag, 1996.

[18] A. Bossi, N. Cocco, and S. Etalle. Transformation of Left Terminating Programs: the Reordering Problem. In M. Proietti, editor, LOPSTR95 – Fifth International Workshop on Logic Program Synthesis and Transformation, number 1048 in LNCS, pages 33–45. Springer-Verlag, 1995.

[19] A. Bossi, N. Cocco, and S. Etalle. Simultaneous replacement in normal programs. Journal of Logic and Computation, 6(1):79–120, February 1996.

[20] A. Bossi and S. Etalle. More on Unfold/Fold Transformations of Normal Programs: Preservation of Fitting’s Semantics. In Proceedings of Meta 94. Springer-Verlag, 1994.

[21] A. Bossi and S. Etalle. Transforming Acyclic Programs. ACM Transactions on Programming Languages and Systems, 16(4):1081–1096, July 1994.

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

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

[24] 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.

[25] M. Cerioli, G. Reggio. Institutions for very abstract specifications. In Recent Trends in Data Type Specification, Lecture Notes in Computer Science 785, 113–127. Springer Verlag, Berlin, 1993.

[26] 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.

[27] E. Coscia and 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.

[28] F.S. de Boer, M. Gabbrielli, E. Marchiori, and C. Palamidessi. Proving Concurrent Constraint Programs Correct. Proc. of the twentieth ACM Symposium on Principles of Programming Languages (POPL), pages 98–108, ACM, 1994.

[29] F.S. de Boer, M. Gabbrielli, and C. Palamidessi. Proving Correctness of Constraint Logic Programs with Dynamic Scheduling. In R. Cousot and D.A. Schmidt, editors, Proc. of the Static Analysis Symposium (SAS 96), volume 1145 of Lecture Notes in Computer Science, pages 83–97. Springer-Verlag, 1996.

[30] F.S. de Boer, J.N. Kok, C. Palamidessi, and J.J.M.M. Rutten. Non-Monotonic Concurrent Constraint Programming. In D. Miller, editor, Proc. of the International Logic Programming Symposium, pages 315–334, The MIT press, 1993.

[31] F.S. de Boer, J.N. Kok, C. Palamidessi, and J.J.M.M. Rutten. A paradigm for asynchronous communication and its application to concurrent constraint programming., Chapter 4 in K. Apt, J.W. de Bakker, and J.J.M.M. Rutten, editors, Logic Programming Languages: Constraints, Functions, and Objects, pages 82–114. Series in Logic Programming, The MIT Press, 1993.

7

[32] F.S. de Boer, J.N. Kok, C. Palamidessi, and J.J.M.M. Rutten. From failure to success: comparing a denotational and a declarative semantics for Horn clause logic, In J.W. de Bakker and J.J.M.M. Rutten, editors, Ten years of concurrency semantics: selected papers of the Amsterdam Concurrency Group. World Scientific Publisher, 1993.

[33] F.S. de Boer, C. Palamidessi. Embedding as a Tool for Language Comparison. Information and Computation. 108(1):128–157, 1994.

[34] F.S. de Boer, C. Palamidessi. From Concurrent Logic Programming to Concurrent Constraint Programming, In G. Levi, editor, Advances in logic programming theory. Oxford University Press, 1994.

[35] F.S. de Boer, C. Palamidessi and A. Di Pierro. Infinite computations in nondeterministic constraint programming. Theoretical Computer Science 151:37–78, 1995.

[36] A. Di Pierro, C. Palamidessi. A Logical Denotational Semantics for Constraint Logic Programming. In D. Sannella, editor, Proc. of Programming Languages and Systems–ESOP. Lecture Notes in Computer Science 788, 195–210. Springer-Verlag, Berlin, 1994.

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

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

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

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

[41] S. Etalle. Unification-free prolog programs revisited. Journal of Programming Languages, (4), 1996. Also in technical report CS-R9454, CWI, Amsterdam.

[42] S. Etalle and M. Gabbrielli. Modular Transformations of CLP Programs. In Proceedings of ICLP 95, pages 681–695, 1995.

[43] S. Etalle and M. Gabbrielli. The replacement operation for CLP modules. In N. Jones, editor, ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM ’95), pages 168–177. ACM press, 1995.

[44] S. Etalle and M. Gabbrielli. Layered modes. In F. de Boer and M. Gabbrielli, editors, Proc. JIC-SLP’96 Post-Conference Workshop on Verification and Analysis of Logic Programs, 1996. Tehcnical Report TR-96-31, Dipartimento di Informatica di Pisa.

[45] S. Etalle and M. Gabbrielli. On the correctness of the replacement operation for clp modules. Journal of Functional and Logic Programming, February 1996. available at, http://www.cs.tuberlin.de/journal/jflp.

[46] S. Etalle and M. Gabbrielli. Transformations of CLP modules. Theoretical Computer Science, 166(1):101–146, 1996.

[47] S. Etalle and F. Teusink. A compositional semantics for normal open programs. In M. Maher, editor, Joint Intermational Conference and Symposium on Logic Programming. MIT-Press, 1996.

[48] M. Falaschi, G. Levi, M. Martelli, C. Palamidessi. A model-theoretic reconstruction of the operational semantics of logic programs. Information and Computation, 103(1):86–113, 1993.

[49] M. Falaschi, M. Gabbrielli, K. Marriott, and C. Palamidessi. Compositional Analysis for Concurrent Constraint Programming. Proc. of the Eight Annual IEEE Symposium on Logic in Computer Science, (LICS), pages 210–221. IEEE Computer Society Press, Los Alamitos, California, 1993.

[50] M. Falaschi, K. Marriott, M. Gabbrielli, and C. Palamidessi. A Simple Semantics for Logic Programming Languages with Dynamic Scheduling. Proc. of the 18th Australian Computer Science Conference (ACSC’95), Adelaide, Australia, 1995.

[51] M. Falaschi, M. Gabbrielli, K. Marriott, and C. Palamidessi. Confluence and Concurrent Constraint Programming. In V.S. Alagar and M. Nivat, editors, Proc. of the Fourth International Conference on Algebraic Methodology and Software Technology (AMAST’95), volume 936 of Lecture Notes in Computer Science, pages 531–545. Springer-Verlag, 1995.

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

[53] R. Giacobazzi, C. Palamidessi, and F. Ranzato. Weak Relative Pseudo-Complements of Closure Operators. Algebra Universalis 36(3): 405–412, 1996.

[54] A. Giordana, L. Saitta, and 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.

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

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

[57] R. McDowell, D. Miller, and C. Palamidessi. Encoding Transition Systems in Sequent Calculus: Preliminary Report Proc. of the Linear Logic Workshop, Tokyo, 29 March–2 April 1996.

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

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

[60] G. Reggio. Event logic for specifying abstract dynamic data types. In M. Bidoit, C. Choppy, editors, Recent Trends in Data Type Specification, Lecture Notes in Computer Science 655, 292–309. Springer Verlag, Berlin, 1993.

[61] M. Bettaz and 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.

[62] 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.

[63] 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.