Type systems

[1] D. Ancona, A. Ferrando, and V. Mascardi. Comparing trace expressions and linear temporal logic for runtime verification. In Theory and Practice of Formal Methods - Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday, pages 47--64, 2016. [ bib | .pdf | Abstract ]
[2] D. Ancona, P. Giannini, and E. Zucca. Incremental rebinding with name polymorphism. Electr. Notes Theor. Comput. Sci., 322:19--34, 2016. [ bib | DOI | .pdf | http | Abstract ]
[3] D. Ancona, V. Bono, M. Bravetti, J. Campos, G. Castagna, P. M. Deniélou, S. J. Gay, N. Gesbert, E. Giachino, R. Hu, E. B. Johnsen, F. Martins, V. Mascardi, F. Montesi, R. Neykova, N. Ng, L. Padovani, V.T. Vasconcelos, and N. Yoshida. Behavioral types in programming languages. Foundations and Trends in Programming Languages, 3(2-3):95--230, 2016. [ bib | DOI | .pdf | http | Abstract ]
[4] Davide Ancona, Daniela Briola, Amal El Fallah-Seghrouchni, Viviana Mascardi, and Patrick Taillibert. Exploiting prolog for projecting agent interaction protocols. In Proceedings of the 29th Italian Conference on Computational Logic, Torino, Italy, June 16-18, 2014., pages 30--45, 2014. [ bib | .pdf | Abstract ]
[5] D. Ancona and A. Corradi. Sound and complete subtyping between coinductive types for object-oriented languages. In ECOOP 2014 - Object-Oriented Programming, 2014. To appear. [ bib | .pdf | Abstract ]
[6] D. Ancona. How to Prove Type Soundness of Java-like Languages Without Forgoing Big-step Semantics. In Formal techniques for Java-like programs (FTfJP14), pages 1:1--1:6. ACM, 2014. [ bib | .pdf | Abstract ]
[7] D. Briola, V. Mascardi, and D. Ancona. Distributed runtime verification of JADE multiagent systems. In Intelligent Distributed Computing VIII - Proceedings of the 8th International Symposium on Intelligent Distributed Computing, IDC 2014, Madrid, Spain, September 3-5, 2014, pages 81--91, 2014. [ bib | .pdf | Abstract ]
[8] D. Ancona, M. Barbieri, and V. Mascardi. Constrained Global Types for Dynamic Checking of Protocol Conformance in Multi-Agent Systems. In ACM Symposium on Applied Computing (SAC 2013), pages 1--3, 2013. Poster paper. [ bib | .pdf | Abstract ]
[9] V. Mascardi, D. Briola, and D. Ancona. On the expressiveness of attribute global types: The formalization of a real multiagent system protocol. In AI*IA 2013: Advances in Artificial Intelligence - XIIIth International Conference of the Italian Association for Artificial Intelligence, Turin, Italy, December 4-6, 2013. Proceedings, pages 300--311, 2013. [ bib | .pdf | Abstract ]
[10] D. Ancona. Soundness of Object-Oriented Languages with Coinductive Big-Step Semantics. In J. Noble, editor, ECOOP 2012 - Object-Oriented Programming, volume 7313, pages 459--483. Springer, 2012. [ bib | .pdf | Abstract ]
[11] D. Ancona and G. Lagorio. Static single information form for abstract compilation. In J. C.M. Baeten, T. Ball, and F. S. de Boer, editors, Theoretical Computer Science (IFIP TCS 2012), volume 7604 of Lecture Notes in Computer Science, pages 10--27. Springer, 2012. [ bib | .pdf | Abstract ]
[12] D. Ancona, M. Barbieri, and V. Mascardi. Global Types for Dynamic Checking of Protocol Conformance of Multi-Agent Systems (Extended Abstract). In P. Massazza, editor, 13th Italian Conference on Theoretical Computer Science (ICTCS 2012), pages 39--43, 2012. [ bib | .pdf | Abstract ]
[13] D. Ancona, S. Drossopoulou, and V. Mascardi. Automatic Generation of Self-Monitoring MASs from Multiparty Global Session Types in Jason. In Declarative agent languages and technologies (DALT 2012)., pages 1--20. Springer, 2012. [ bib | .pdf | Abstract ]
[14] D. Ancona, A. Corradi, G. Lagorio, and F. Damiani. Abstract compilation of object-oriented languages into coinductive CLP(X): can type inference meet verification? In B. Beckert and C. Marché, editors, Formal Verification of Object-Oriented Software International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010, Revised Selected Papers, volume 6528 of Lecture Notes in Computer Science. Springer Verlag, 2011. [ bib | .pdf | Abstract ]
[15] D. Ancona and G. Lagorio. Idealized coinductive type systems for imperative object-oriented programs. RAIRO - Theoretical Informatics and Applications, 45(1):3--33, 2011. [ bib | .pdf | http | Abstract ]
[16] D. Ancona. Coinductive big-step operational semantics for type soundness of Java-like languages. In Formal Techniques for Java-like Programs (FTfJP11), pages 5:1--5:6. ACM, 2011. [ bib | .pdf | Abstract ]
[17] V. Mascardi and D Ancona. 1000 years of coo-BDI. In Declarative Agent Languages and Technologies IX - 9th International Workshop, DALT 2011, Revised Selected and Invited Papers, pages 95--101, 2011. [ bib | .pdf | Abstract ]
[18] V. Mascardi, D. Ancona, R. H. Bordini, and A. Ricci. Cool-AgentSpeak: Enhancing AgentSpeak-DL Agents with Plan Exchange and Ontology Services. In Proceedings of the 2011 IEEE/WIC/ACM International Conference on Intelligent Agent Technology, IAT 2011, pages 109--116, 2011. [ bib | .pdf | Abstract ]
[19] D. Ancona and G. Lagorio. On sound and complete axiomatization of coinductive subtyping for object-oriented languages. Technical report, DISI, November 2010. Submitted for journal publication. Extended version of FTfJP10. [ bib | .pdf | Abstract ]
[20] D. Ancona, A. Corradi, G. Lagorio, and F. Damiani. Abstract compilation of object-oriented languages into coinductive CLP(X): can type inference meet verification? (extended version). Technical report, DISI, August 2010. Extended version of FoVeOOS10. [ bib | .pdf | Abstract ]
[21] D. Ancona and G. Lagorio. Complete coinductive subtyping for abstract compilation of object-oriented languages. In FTFJP '10: Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, ACM Digital Library, pages 1:1--1:7. ACM, 2010. [ bib | .pdf | http | Abstract ]
[22] D. Ancona and G. Lagorio. Coinductive subtyping for abstract compilation of object-oriented languages into Horn formulas. In Montanari A., Napoli M., and Parente M., editors, Proceedings of GandALF 2010, volume 25 of Electronic Proceedings in Theoretical Computer Science, pages 214--223, 2010. [ bib | .pdf | Abstract ]
[23] D. Ancona, A. Corradi, G. Lagorio, and F. Damiani. Abstract compilation of object-oriented languages into coinductive CLP(X): when type inference meets verification. Technical report, Karlsruhe Institute of Technology, 2010. Formal Verification of Object-Oriented Software. Papers presented at the International Conference, June 28-30, 2010, Paris, France. [ bib | .pdf | Abstract ]
[24] D. Ancona, G. Lagorio, and E. Zucca. Type inference by coinductive logic programming. In de' Liguoro U. Berardi S., Damiani F., editor, Post-Proceedings of TYPES 2008, volume 5497 of Lecture Notes in Computer Science. Springer Verlag, 2009. [ bib | .pdf | Abstract ]
[25] D. Ancona and G. Lagorio. Coinductive type systems for object-oriented languages. In S. Drossopoulou, editor, ECOOP 2009 - Object-Oriented Programming, volume 5653 of Lecture Notes in Computer Science, pages 2--26. Springer Verlag, 2009. Best paper prize. [ bib | .pdf | Abstract ]
[26] D. Ancona and V. Mascardi. Ontology matching for semi-automatic and type-safe adaptation of Java programs. Technical report, DISI - Univ. of Genova, December 2008. [ bib | .pdf | Abstract ]
[27] D. Ancona, G. Lagorio, and E. Zucca. Type inference for Java-like programs by coinductive logic programming. Technical report, DISI - Univ. of Genova, July 2008. [ bib | .pdf | Abstract ]
[28] D. Ancona, G. Lagorio, and E. Zucca. A flexible and type-safe framework of components for Java-like languages. Technical report, DISI - Univ. of Genova, April 2008. Submitted for journal publication. Extended version of JMLC06. [ bib | .pdf | Abstract ]
[29] D. Ancona, S. Fagorzi, and E. Zucca. A parametric calculus for mobile open code. Electronic Notes in Theoretical Computer Science, 192(3):3 -- 22, 2008. Proceedings of the Third International Workshop on Developments in Computational Models (DCM 2007). [ bib | DOI | .pdf | http | Abstract ]
[30] D. Ancona, C. Anderson, F. Damiani, S. Drossopoulou, P. Giannini, and E. Zucca. A Provenly Correct Translation of Fickle into Java. ACM Transactions on Programming Languages and Systems, 29(2), April 2007. [ bib | .pdf | Abstract ]
[31] D. Ancona, G. Lagorio, and E. Zucca. Type inference for polymorphic methods in Java-like languages. In G. Italiano, E. Moggi, and L. Laura, editors, Theoretical Computer Science: Proceedings of the 10th Italian Conference on ICTCS '07. World Scientific, 2007. See also the long version with proofs. [ bib | .pdf | Abstract ]
[32] D. Ancona and E. Zucca. A formal framework for compositional compilation (extended abstract). In D. Ancona, G. Lagorio, and E. Zucca, editors, Theoretical Computer Science: Proceedings of the 10th Italian Conference on ICTCS '07. World Scientific, 2007. See also the long version with proofs and examples of framework instantiation. [ bib | .pdf | Abstract ]
[33] D. Ancona, G. Lagorio, and E. Zucca. Flexible type-safe linking of components for Java-like languages. In Joint Modular Languages Conference (JMLC 2006), volume 4228 of Lecture Notes in Computer Science, pages 136--154. Springer Verlag, 2006. See also the extended version. [ bib | .pdf | Abstract ]
[34] D. Ancona, G. Lagorio, and E. Zucca. Smart modules for Java-like languages. In 7th Intl. Workshop on Formal Techniques for Java-like Programs 2005, July 2005. [ bib | .pdf | Abstract ]
[35] D. Ancona, F. Damiani, S. Drossopoulou, and E. Zucca. Compositional Compilation for Java-like Languages through Polymorphic Bytecode. Technical report, Dipartimento di Informatica e Scienze dell'Informazione, Università di Genova, January 2005. [ bib | .pdf | Abstract ]
[36] D. Ancona, F. Damiani, S. Drossopoulou, and E. Zucca. Polymorphic bytecode: Compositional compilation for Java-like languages. In POPL 2005 - The 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 26--37. ACM Press, 2005. [ bib | .pdf | Abstract ]
[37] D. Ancona, S. Fagorzi, and E. Zucca. Mixin modules for dynamic rebinding. In R. De Nicola and D. Sangiorgi, editors, Trustworthy Global Computing: IST/FET International Workshop, TGC 2005, Edinburgh, UK, April 7-9, 2005. Revised Selected Papers, volume 3705 of Lecture Notes in Computer Science, pages 279--298. Springer Verlag, 2005. [ bib | .pdf | Abstract ]
[38] D. Ancona and E. Moggi. Program Generation and Components. In F. S. de Boer, M. M. Bonsangue, S. Graf, and W. de Roever, editors, Formal Methods for Components and Objects: Third International Symposium, FMCO 2004, volume 3657 of Lecture Notes in Computer Science, pages 222--250. Springer Verlag, 2005. [ bib | .pdf | Abstract ]
[39] D. Ancona, S. Fagorzi, and E. Zucca. A calculus for dynamic reconfiguration with low priority linking. Electronic Notes in Theoretical Computer Science. Proceedings of the Second Workshop on Object Oriented Developments (WOOD 2004), 138(2):3--35, 2005. [ bib | .pdf | http | Abstract ]
[40] D. Ancona and G. Lagorio. Stronger Typings for Smarter Recompilation of Java-like Languages. Journal of Object Technology. Special issue. Workshop on Formal Techniques for Java-like Programs (FTfJP) ECOOP 2003, 3(6):5--25, June 2004. [ bib | .ps.gz | http | http | Abstract ]
[41] D. Ancona, F. Damiani, S. Drossopoulou, and E. Zucca. Even more principal typings for Java-like languages. In 6th Intl. Workshop on Formal Techniques for Java Programs 2004, June 2004. [ bib | .pdf | Abstract ]
[42] D. Ancona and E. Moggi. A Fresh Calculus for Name Management. In G. Karsai and E. Visser, editors, Generative Programming and Component Engineering (GPCE 2004), volume 3286 of Lecture Notes in Computer Science, pages 206--224. Springer Verlag, 2004. [ bib | .pdf | Abstract ]
[43] S. Fagorzi, E. Zucca, and D. Ancona. Modeling multiple class loaders by a calculus for dynamic linking. In H. Haddad, A. Omicini, R. L. Wainwright, and L. M. Liebrock, editors, SAC 2004 - Proceedings of the 2004 ACM Symposium on Applied Computing, pages 1281--1288. ACM Press, 2004. [ bib | .ps.gz | Abstract ]
[44] D. Ancona and E. Zucca. Principal typings for Java-like languages. In POPL 2004 - The 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 306--317. ACM Press, 2004. [ bib | .ps.gz | Abstract ]
[45] D. Ancona, S. Fagorzi, and E. Zucca. A calculus with lazy module operators. In J.-J. Levy, E. W. Mayr, and J. C. Mitchell, editors, IFIP 18th World Computer Congress, TC1 3rd Int. Conf. on Theoretical Computer Science (TCS2004), pages 423--436. Kluwer Academic Publishers, 2004. [ bib | .pdf | Abstract ]
[46] D. Ancona, G. Lagorio, and E. Zucca. Jam--designing a Java extension with mixins. ACM Transactions on Programming Languages and Systems, 25(5):641--712, September 2003. [ bib | .ps.gz | http | Abstract ]
[47] D. Ancona, S. Fagorzi, E. Moggi, and E. Zucca. Mixin modules and computational effects. In G. Goos, J. Hartmanis, and J. van Leeuwen, editors, ICALP 2003 - Automata, Languages and Programming, volume 2719 of Lecture Notes in Computer Science, pages 224--238. Springer Verlag, 2003. [ bib | .ps.gz | Abstract ]
[48] D. Ancona and G. Lagorio. Stronger typings for separate compilation of Java-like languages (Extended Abstract). In 5th Intl. Workshop on Formal Techniques for Java Programs 2003, 2003. [ bib | .ps.gz | http | .html | Abstract ]
[49] D. Ancona, S. Fagorzi, and E. Zucca. A calculus for dynamic linking. In C. Blundo and C. Laneve, editors, ICTCS 2003 - Theoretical Computer Science, volume 2841 of Lecture Notes in Computer Science, pages 284--301. Springer Verlag, 2003. [ bib | .ps.gz | Abstract ]
[50] D. Ancona, G. Lagorio, and E. Zucca. Simplifying types for a calculus of Java exceptions. Technical report, Dipartimento di Informatica e Scienze dell'Informazione, Università di Genova, August 2002. Submitted for journal publication. [ bib | .ps.gz | Abstract ]
[51] D. Ancona and E. Zucca. A calculus of module systems. Journ. of Functional Programming, 12(2):91--132, 2002. [ bib | .ps.gz | .html | Abstract ]
[52] D. Ancona, G. Lagorio, and E. Zucca. True separate compilation of Java classes. In ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'02), pages 189--200. ACM Press, 2002. [ bib | .ps.gz | Abstract ]
[53] D. Ancona, G. Lagorio, and E. Zucca. A formal framework for Java separate compilation. In B. Magnusson, editor, ECOOP 2002 - Object-Oriented Programming, volume 2374 of Lecture Notes in Computer Science, pages 609--635. Springer Verlag, 2002. [ bib | .ps.gz | Abstract ]
[54] D. Ancona, C. Anderson, F. Damiani, S. Drossopoulou, P. Giannini, and E. Zucca. A type preserving translation of Fickle into Java. Electronic Notes in Theoretical Computer Science. TOSCA 2001, Theory of Concurrency, Higher Order Languages and Types, 62:69--82, 2002. [ bib | .ps.gz | http | Abstract ]
[55] D. Ancona and E. Zucca. True modules for Java-like languages. In J.L. Knudsen, editor, ECOOP 2001 - Object-Oriented Programming, volume 2072 of Lecture Notes in Computer Science, pages 354--380. Springer Verlag, 2001. [ bib | .ps.gz | Abstract ]
[56] D. Ancona, G. Lagorio, and E. Zucca. Java separate type checking is not safe. In 3rd Intl. Workshop on Formal Techniques for Java Programs 2001, 2001. [ bib | .ps.gz | http | Abstract ]
[57] D. Ancona, C. Anderson, F. Damiani, S. Drossopoulou, P. Giannini, and E. Zucca. An effective translation of Fickle into Java. In A. Restivo, S. Ronchi Della Rocca, and L. Roversi, editors, ICTCS 2001 - Theoretical Computer Science, volume 2202 of Lecture Notes in Computer Science, pages 215--234. Springer Verlag, 2001. [ bib | .ps.gz | Abstract ]
[58] D. Ancona, G. Lagorio, and E. Zucca. A core calculus for Java exceptions. In ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA 2001), SIGPLAN Notices. ACM Press, 2001. [ bib | .ps.gz | Abstract ]
[59] D. Ancona, E. Zucca, and S. Drossopoulou. Overloading and inheritance. In The Eighth International Workshop on Foundations of Object-Oriented Languages (FOOL8), 2001. [ bib | .ps.gz | Abstract ]
[60] D. Ancona, G. Lagorio, and E. Zucca. Jam: A smooth extension of Java with mixins. In E. Bertino, editor, ECOOP 2000 - Object-Oriented Programming, volume 1850 of Lecture Notes in Computer Science, pages 154--178. Springer Verlag, 2000. [ bib | .ps.gz | http | Abstract ]
[61] D. Ancona, G. Lagorio, and E. Zucca. A core calculus for Java exceptions (Extended Abstract). In 2nd Intl. Workshop on Formal Techniques for Java Programs 2000, 2000. [ bib | .pdf | http | Abstract ]
[62] D. Ancona, E. Zucca, and S. Drossopoulou. Overloading and inheritance in Java (Extended Abstract). In 2nd Intl. Workshop on Formal Techniques for Java Programs 2000, 2000. [ bib | .pdf | http | Abstract ]
[63] D. Ancona and V. Mascardi. Mixin-based modules for logic programming. In APPIA-GULP-PRODE 2000. 2000 Joint Conference on Declarative Programming, 2000. [ bib | .ps.gz | Abstract ]
[64] D. Ancona and E. Zucca. A primitive calculus for module systems. In G. Nadathur, editor, PPDP'99 - International Conference of Principles and Practice of Declarative Programming, volume 1702 of Lecture Notes in Computer Science, pages 62--79. Springer Verlag, 1999. [ bib | .ps.gz | .html | Abstract ]
[65] D. Ancona. An algebraic framework for separate type-checking. In J. Fiadeiro, editor, WADT'98 - 13th Workshop on Algebraic Development Techniques - Selected Papers, volume 1589 of Lecture Notes in Computer Science, pages 1--15. Springer Verlag, 1999. [ bib | .ps.gz | Abstract ]

This file was generated by bibtex2html 1.98.


Back to the main page on Davide Ancona's papers

Please send suggestions and comments to:
Davide Ancona davide.ancona@unige.it

Last Updated: January 2017