Publications by Marino Miculan

• A categorical model of the Fusion calculus.
  In Proceedings of MFPS XXIV, ENTCS ?, pp. ?-?, Elsevier, 2008. (Final proceedings version).
• PicNIc - Pi-calculus Non-Interference checker. (With Silvia Crafa, Matteo Mio, Carla Piazza, Sabina Rossi)
  J. Billington and M. Koutny, editors, 8th International Conference on Application of Concurrency to System Design, Proceedings. IEEE, 2008.
• Implementing Spi Calculus using Nominal techniques. (With Temesghen Kahsai)
  In Arnold Beckmann, Costas Dimitracopoulos, and Benedikt Löwe, editors, Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, CiE 2008, Athens, Greece, June 2008, Proceedings. Lecture Notes in Computer Science volume 5028, 2008.
• An Algebra for Directed Bigraphs. (With Davide Grohmann)
  In I. Mackie and D. Plump, editors, Proceedings of TERMGRAPH 2007, ENTCS 203(1), pp. 49-63, 2008.
• Controlling resource access in Directed Bigraphs. (With Davide Grohmann)
  Claudia Ermel, Reiko Heckel, and Juan de Lara, editors, Proceedings of GT-VMT 2008, Electronic Communications of the EASST, Volume 10 (2008).
  A longer version with appendixes is available.

• Undecidability of Model checking in Brane Logic. (With Giorgio Bacci.)
  In Dezani and Danos, editors, Pre-Proceedings of DCM'07.
• Reactive Systems over Directed Bigraphs. (With Davide Grohmann)
  L. Caires and V.T. Vasconcelos, editors, Proceedings of CONCUR 2007, Number 4703 in Lecture Notes in Computer Science, pages 380-394, 2007.
  
• Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts. (With Alberto Ciaffaglione and Luigi Liquori.)
  Journal of Automated Reasoning, Volume 39(1), pp. 1-47, July 2007.
• Directed Bigraphs. (With Davide Grohmann)
  In Proceedings of MFPS XXIII, ENTCS 173, pp. 121-137, Elsevier, 2007.

• Directed Bigraphs: Theory and Applications. (With Davide Grohmann.)
  DiMI Research Report UDMI/12/2006/RR, University of Udine, December 2006.
• About permutation algebras, (pre)sheaves and named sets. (With Fabio Gadducci, Ugo Montanari.)
  Higher Order and Symbolic Computation, Volume 19, Numbers 2-3, September 2006, pp 283-304
• Modal logics for Brane Calculus. (With Giorgio Bacci.)
  In C. Priami, editor, Proceedings of CMSB'06. Number 4210 in Lecture Notes in Computer Science, pages 1-16, 2006.
  Slides. An extended version is available as Research Report UDMI/08/2006/RR.
• Consistency of the Theory of Contexts. (With Anna Bucalo, Martin Hofmann, Furio Honsell, Ivan Scagnetto.)
  Journal of Functional Programming, Volume 16, Issue 03, May 2006, pp 327-395

• Implementazione di Memoria Distribuita su cluster CompactPCI. (With Maja Massarini and Francesco Sepic.)
  In Atti del Congresso AICA 2005.
• Translating Specifications from Nominal Logic to CIC with the Theory of Contexts. (With Ivan Scagnetto, Furio Honsell.)
  In R. Pollack, editor, Proceedings of MERLIN'05. ACM DL, 2005.
  Slides, Coq code.
• A unifying model of variables and names. (With Kidane Yemane.)
  In V. Sassone, editor, Proceedings of FOSSACS'05. Number 3441 in Lecture Notes in Computer Science, pages 170-186, 2005.
  An extended version is available as (revised) Research Report UDMI/15/2004/RR.

• Modeling Fresh Names in the π-calculus using Abstractions. (With Roberto Bruni, Furio Honsell, Marina Lenisa.)
  In Proceedings of CMCS 2004. ENTCS 106, pages 25-41, Elsevier, 2004.
• Unifying Recursive and Co-recursive Definitions in Sheaf Categories. (With Pietro Di Gianantonio.)
  In I. Walukiewicz, editor, Proceedings of FOSSACS'04. Number 2987 in Lecture Notes in Computer Science, 2004.
• Proceedings of CoMeta 2003 (editor, with Furio Honsell, Marina Lenisa.)
  15-17 December 2003, Udine. Elsevier ENTCS 104, 2004.
• Some characterization results for permutation algebras. (With Fabio Gadducci, Ugo Montanari.)
  In Proceedings of COMETA 2003. ENTCS 104, 2003. Elsevier.
  An extended version is available as Research Report UDMI/26/2003/RR.

• A Framework for Typed HOAS and Semantics. (With Ivan Scagnetto.)
  In Proceedings of PPDP 2003, pages 184–194. Uppsala, 2003. ACM.
• Reasoning on an Imperative Object-based Calculus in Higher Order Abstract Syntax. (With Alberto Ciaffaglione and Luigi Liquori.)
  In Proceedings of MERλIN 2003. ACM, 2003.
• Proceedings of MERλIN 2003 (editor, with Furio Honsell, Alberto Momigliano.)
  26 August 2003, Uppsala. ACM, 2003.
• Imperative Object-based Calculi in (Co)Inductive Type Theories. (With Alberto Ciaffaglione and Luigi Liquori.)
  In Proceedings of LPAR 2003, LNCS 2850, pages 59–77, 2003.
  An extended version is available as Research report RR-4812, INRIA-Lorraine, 2003.
• Special Issue of Theoretical Computer Science on FOSSACS 2001 (editor, with Furio Honsell).
  TCS 283, Elsevier, 2003.

• A Unifying Approach to Recursive and Co-recursive Definitions. (With Pietro Di Gianantonio.)
  In Geuvers, Wiedijk, editors, Proceedings of TYPES'02. Number 2646 in Lecture Notes in Computer Science, 2003. Coq code.
• Ambient Calculus and its Logic in the Calculus of Inductive Constructions. (With Ivan Scagnetto.)
  In Proceedings of LFM 2002. ENTCS 70.2, Elsevier, 2002.
  Slides, Coq code.
• Frecuencis lessicâls dal furlan scrit. (With Alessandra Burelli). In Gjornâl furlan des siencis - Friulian journal of science, Vol. 1, March 2002.

• The Theory of Contexts for First Order and Higher Order Abstract Syntax. (With Furio Honsell, Ivan Scagnetto.)
  In Proceedings of TOSCA 2001. ENTCS 62, Elsevier/Forum, 2001.
• Comparing Higher-order Encodings in Logical Frameworks and Tile Logic. (With Roberto Bruni, Furio Honsell, Marina Lenisa.)
  In Proceedings of TOSCA 2001. ENTCS 62, Elsevier/Forum, 2001.
• Developing (Meta)Theory of lambda-calculus in the Theory of Contexts.
  In Proceedings of the Workshop on MEchanized Reasoning about Languages with variable bINding (MERLIN 2001). ENTCS 58.1, Elsevier, 2001.
  Slides, Coq code.
• An axiomatic approach to metareasoning on systems in higher-order abstract syntax. (With Furio Honsell, Ivan Scagnetto.)
  In Proceedings of ICALP'01, Number 2076 in Lecture Notes in Computer Science, pages 963-978, 2001 (slightly expanded version).
  Slides.
• Proceedings of FOSSACS 2001 (editor, with Furio Honsell).
  LNCS 2030, Springer-Verlag, 2001.
• On the formalization of the modal μ-calculus in the Calculus of Inductive Constructions.
  In Information and Computation, Vol. 164, No. 1, pages 199-231, 2001.
• π-calculus in (Co)Inductive Type Theories. (With Furio Honsell, Ivan Scagnetto.)
  In Theoretical Computer Science, 253(2), pages 239-285, 2001.

• The Journal of High Energy Physics: Scientific Publishing on the Web. (With Fabio Asnicar, Marina Candusso, Simona Cerrato, Paolo Dall'Aglio, Amanda de Felice, Massimo Di Fant, Marco Mizzaro, Fabrizio Nesti.)
  In WebNet (2) 1999: 1482-1483. 1999.
• Formalizing a lazy substitution proof system for μ-calculus in the Calculus of Inductive Constructions.
  In Proceedings of ICALP'99. Number 1644 in Lecture Notes in Computer Science, pages 554-564, 1999. Coq code.

• A Natural Deduction style proof system for propositional μ-calculus and its formalization in inductive type theories.
  In Proceedings of ICTCS'98. World Scientific, 1998.
• Encoding Modal Logics in Logical Frameworks. (With Arnon Avron, Furio Honsell, Cristian Paravano.)
  In Studia Logica, 60(1), Jan. 1998.

• Encoding Logical Theories of Programs.
  Ph.D. Thesis TD-7/97, March 1997. Dipartimento di Informatica, Università di Pisa.
• A Natural Deduction Approach to Dynamic Logics. (With Furio Honsell).
  In Berardi, Coppo, editors, Proceedings of TYPES'95. Number 1158 in Lecture Notes in Computer Science, p.165-182, 1996. See also the Coq code.
• Modal μ-types for Processes. (With Fabio Gadducci.)
  In Proceedings of Tenth Annual IEEE Symposium on Logic in Computer Science, pages 221-231, San Diego, California, 26-29 June 1995. IEEE Computer Society Press.
• Expressivity of Structured Operational Semantics with Explicit Assumptions.
  In Barendregt, Nipkow, editors, Proceedings of TYPES'93. Number 806 in Lecture Notes in Computer Science, p.292-320, 1994.

Other presentations and talks

1. FLOSS nella ricerca.
   Slides of talk given at the conference Il software libero in Friuli Venezia Giulia, Udine, 7 febbraio 2008. In Italian.
2. Licenze software e Open Source.
   Slides of talk given at the Ciclo di seminari ALSI 2007, Udine, 18 Luglio 2007. In Italian.
3. Si fa presto a dire Open Source.
   OpenOffice (Impress) slides of talk given at the Convegno ALSI 2002 su Soluzioni Open Source per le Aziende, Udine, December 13, 2002. In Italian. Also available as zipped PDF, two or six slides per page.
4. Towards a general framework for metareasoning on HOAS encodings. (With Anna Bucalo, Martin Hofmann, Furio Honsell, Ivan Scagnetto.)
   Slides of talk given at the TOSCA'00 Workshop, Genova, December 1, 2000.