Publications

2015

  • Giorgio Bacci and Marino Miculan. Structural operational semantics for continuous state stochastic transition systems. Journal of computer and system sciences, 81:834-858, 2015.
    [Bibtex] [DOI] [url]
    @article{Bacci2014,
    Abstract = {Abstract In this paper we show how to model syntax and semantics of stochastic processes with continuous states, respectively as algebras and coalgebras of suitable endofunctors over the category of measurable spaces Meas. Moreover, we present an SOS-like rule format, called MGSOS, representing abstract \{GSOS\} over Meas, and yielding fully abstract universal semantics, for which behavioral equivalence is a congruence. An \{MGSOS\} specification defines how semantics of processes are composed by means of measure terms, which are expressions specifically designed for describing finite measures. The syntax of these measure terms, and their interpretation as measures, are part of the \{MGSOS\} specification. We give two example applications, with a simple and neat \{MGSOS\} specification: a ``quantitative CCS'', and a calculus of processes living in the plane R 2 whose communication rate depends on their distance. The approach we follow in these cases can be readily adapted to deal with other quantitative aspects. },
    Author = {Giorgio Bacci and Marino Miculan},
    Date-Added = {2015-01-15 10:14:19 +0000},
    Date-Modified = {2015-01-15 11:26:24 +0000},
    Doi = {http://dx.doi.org/10.1016/j.jcss.2014.12.003},
    Issn = {0022-0000},
    Journal = {Journal of Computer and System Sciences},
    Keywords = {Quantitative aspects},
    Pages = {834-858},
    Title = {Structural operational semantics for continuous state stochastic transition systems},
    Url = {http://www.sciencedirect.com/science/article/pii/S0022000014001652},
    Volume = 81,
    Year = {2015},
    Bdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/S0022000014001652},
    Bdsk-Url-2 = {http://dx.doi.org/10.1016/j.jcss.2014.12.003}}
  • Marino Miculan, Marco Peressotti, and Andrea Toneguzzo. Open transactions on shared memory. In Coordination models and languages – 17th IFIP WG 6.1 international conference, COORDINATION 2015, held as part of the 10th international federated conference on distributed computing techniques, discotec 2015, grenoble, france, june 2-4, 2015, proceedings, pages 213-229, 2015.
    [Bibtex] [PDF] [DOI] [url]
    @inproceedings{mpt:coord15,
    Author = {Marino Miculan and Marco Peressotti and Andrea Toneguzzo},
    Bibsource = {dblp computer science bibliography, http://dblp.org},
    Biburl = {http://dblp.uni-trier.de/rec/bib/conf/coordination/MiculanPT15},
    Booktitle = {Coordination Models and Languages - 17th {IFIP} {WG} 6.1 International Conference, {COORDINATION} 2015, Held as Part of the 10th International Federated Conference on Distributed Computing Techniques, DisCoTec 2015, Grenoble, France, June 2-4, 2015, Proceedings},
    Crossref = {DBLP:conf/coordination/2015},
    Doi = {10.1007/978-3-319-19282-6_14},
    Pages = {213--229},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/COORDINATION15.pdf},
    Timestamp = {Thu, 30 Apr 2015 16:05:22 +0200},
    Title = {Open Transactions on Shared Memory},
    Url = {http://dx.doi.org/10.1007/978-3-319-19282-6_14},
    Year = {2015},
    Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-319-19282-6_14}}
  • Tomasz Brengos, Marino Miculan, and Marco Peressotti. Behavioural equivalences for coalgebras with unobservable moves. Journal of logical and algebraic methods in programming, page -, 2015.
    [Bibtex] [PDF] [DOI] [url]
    @article{bmp:jlamp15,
    title = "Behavioural equivalences for coalgebras with unobservable moves ",
    journal = "Journal of Logical and Algebraic Methods in Programming ",
    volume = "",
    number = "",
    pages = " - ",
    year = "2015",
    note = "",
    issn = "2352-2208",
    doi = "10.1016/j.jlamp.2015.09.002",
    url = "http://arxiv.org/abs/1411.0090",
    pdf = "http://arxiv.org/pdf/1411.0090v3",
    author = "Tomasz Brengos and Marino Miculan and Marco Peressotti",
    keywords = "Process calculi",
    keywords = "Coalgebraic semantics",
    keywords = "Weak behavioural equivalences",
    keywords = "Saturation semantics ",
    abstract = "We introduce a general categorical framework for the definition of weak behavioural equivalences, building on and extending recent results in the field. This framework is based on special order enriched categories, i.e. categories whose hom-sets are endowed with suitable complete orders. Using this structure we provide an abstract notion of saturation, which allows us to define various (weak) behavioural equivalences. We show that the Kleisli categories of many common monads are categories of this kind. On one hand, this allows us to instantiate the abstract definitions to a wide range of existing systems (weighted LTS, Segala systems, calculi with names, etc.), recovering the corresponding notions of weak behavioural equivalences; on the other, we can readily provide new weak behavioural equivalences for more complex behaviours, like those definable on presheaves, topological spaces, measurable spaces, etc. "
    }
  • Stefano Mizzaro, Marco Pavan, and Ivan Scagnetto. Content-based similarity of twitter users. In Allan Hanbury, Gabriella Kazai, Andreas Rauber, and Norbert Fuhr, editors, Advances in information retrieval, volume 9022 of Lecture Notes in Computer Science, pages 507-512. Springer International Publishing, 2015.
    [Bibtex] [DOI] [url]
    @incollection{mps:air15,
    year={2015},
    isbn={978-3-319-16353-6},
    booktitle={Advances in Information Retrieval},
    volume={9022},
    series={Lecture Notes in Computer Science},
    editor={Hanbury, Allan and Kazai, Gabriella and Rauber, Andreas and Fuhr, Norbert},
    doi={10.1007/978-3-319-16354-3_56},
    title={Content-Based Similarity of Twitter Users},
    url={http://dx.doi.org/10.1007/978-3-319-16354-3_56},
    publisher={Springer International Publishing},
    author={Mizzaro, Stefano and Pavan, Marco and Scagnetto, Ivan},
    pages={507-512},
    language={English}
    }
  • Alberto Ciaffaglione and Ivan Scagnetto. Mechanizing type environments in weak hoas. Theoretical computer science, page -, 2015.
    [Bibtex] [DOI] [url]
    @article{Ciaffaglione2015,
    title = "Mechanizing type environments in weak HOAS",
    journal = "Theoretical Computer Science ",
    volume = "",
    number = "",
    pages = " - ",
    year = "2015",
    note = "",
    issn = "0304-3975",
    doi = "http://dx.doi.org/10.1016/j.tcs.2015.07.019",
    url = "http://www.sciencedirect.com/science/article/pii/S0304397515006404",
    author = "Alberto Ciaffaglione and Ivan Scagnetto",
    keywords = "Type theory",
    keywords = "Logical frameworks",
    keywords = "HOAS",
    keywords = "POPLmark challenge ",
    abstract = "Abstract We provide a paradigmatic case study, about the formalization of System F < : 's type language in the proof assistant Coq. Our approach relies on weak HOAS, for the sake of producing a readable and concise representation of the object language. Actually, we present and discuss two encoding strategies for typing environments which yield a remarkable influence on the whole formalization. Then, on the one hand we develop System F < : 's metatheory, on the other hand we address the equivalence of the two approaches internally to Coq. "
    }
  • Furio Honsell, Luigi Liquori, Petar Maksimović, and Ivan Scagnetto. Gluing together proof environments: canonical extensions of lf type theories featuring locks. In Iliano Cervesato and Kaustuv Chaudhuri, editors, Proceedings tenth international workshop on logical frameworks and meta languages: theory and practice, berlin, germany, 1 august 2015, volume 185 of Electronic Proceedings in Theoretical Computer Science, pages 3-17. Open Publishing Association, 2015.
    [Bibtex] [DOI]
    @Inproceedings{EPTCS185.1,
    author = "Honsell, Furio and Liquori, Luigi and Maksimovi\'c, Petar and Scagnetto, Ivan",
    year = "2015",
    title = "Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks",
    editor = "Cervesato, Iliano and Chaudhuri, Kaustuv",
    booktitle = "Proceedings Tenth International Workshop on
    Logical Frameworks and Meta Languages: Theory and Practice,
    Berlin, Germany, 1 August 2015",
    series = "Electronic Proceedings in Theoretical Computer Science",
    volume = "185",
    publisher = "Open Publishing Association",
    pages = "3-17",
    doi = "10.4204/EPTCS.185.1",
    }

2014

  • Tomasz Brengos, Marino Miculan, and Marco Peressotti. Behavioural equivalences for coalgebras with unobservable moves. Corr, abs/1411.0090, 2014.
    [Bibtex] [url]
    @article{DBLP:journals/corr/BrengosMP14,
    Author = {Tomasz Brengos and Marino Miculan and Marco Peressotti},
    Bibsource = {dblp computer science bibliography, http://dblp.org},
    Biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/BrengosMP14},
    Date-Added = {2015-01-15 11:16:02 +0000},
    Date-Modified = {2015-01-15 11:16:02 +0000},
    Journal = {CoRR},
    Timestamp = {Mon, 01 Dec 2014 14:32:13 +0100},
    Title = {Behavioural equivalences for coalgebras with unobservable moves},
    Url = {http://arxiv.org/abs/1411.0090},
    Volume = {abs/1411.0090},
    Year = {2014},
    Bdsk-Url-1 = {http://arxiv.org/abs/1411.0090}}
  • Marino Miculan and Marco Peressotti. GSOS for non-deterministic processes with quantitative aspects. In Nathalie Bertrand and Luca Bortolussi, editors, Proceedings twelfth international workshop on quantitative aspects of programming languages and systems, QAPL 2014, grenoble, france, 12-13 april 2014., volume 154 of EPTCS, pages 17-33, 2014.
    [Bibtex] [DOI] [url]
    @inproceedings{DBLP:journals/corr/MiculanP14,
    Author = {Marino Miculan and Marco Peressotti},
    Bibsource = {dblp computer science bibliography, http://dblp.org},
    Biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/MiculanP14},
    Booktitle = {Proceedings Twelfth International Workshop on Quantitative Aspects of Programming Languages and Systems, {QAPL} 2014, Grenoble, France, 12-13 April 2014.},
    Date-Added = {2015-01-15 11:04:40 +0000},
    Date-Modified = {2015-01-15 11:05:13 +0000},
    Doi = {10.4204/EPTCS.154.2},
    Editor = {Nathalie Bertrand and Luca Bortolussi},
    Pages = {17--33},
    Series = {EPTCS},
    Timestamp = {Tue, 01 Jul 2014 17:30:23 +0200},
    Title = {{GSOS} for non-deterministic processes with quantitative aspects},
    Url = {http://dx.doi.org/10.4204/EPTCS.154.2},
    Volume = {154},
    Year = {2014},
    Bdsk-Url-1 = {http://dx.doi.org/10.4204/EPTCS.154.2}}
  • Alessio Mansutti, Marino Miculan, and Marco Peressotti. Towards distributed bigraphical reactive systems. In Rachid Echahed, Annegret Habel, and Mohamed Mosbah, editors, Proc. gcm’14. EPTCS, 2014.
    [Bibtex]
    @inproceedings{mmp:gcm14,
    Author = {Alessio Mansutti and Marino Miculan and Marco Peressotti},
    Booktitle = {Proc. GCM'14},
    Date-Added = {2015-01-15 10:58:53 +0000},
    Date-Modified = {2015-01-15 11:55:14 +0000},
    Editor = {Rachid Echahed and Annegret Habel and Mohamed Mosbah},
    Publisher = {EPTCS},
    Title = {Towards distributed bigraphical reactive systems},
    Year = {2014}}
  • Marino Miculan and Marco Peressotti. A CSP implementation of the bigraph embedding problem. Corr, abs/1412.1042, 2014.
    [Bibtex] [url]
    @article{DBLP:journals/corr/MiculanP14b,
    Author = {Marino Miculan and Marco Peressotti},
    Bibsource = {dblp computer science bibliography, http://dblp.org},
    Biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/MiculanP14b},
    Date-Added = {2015-01-15 10:49:57 +0000},
    Date-Modified = {2015-01-15 10:49:57 +0000},
    Journal = {CoRR},
    Timestamp = {Thu, 01 Jan 2015 19:51:08 +0100},
    Title = {A {CSP} implementation of the bigraph embedding problem},
    Url = {http://arxiv.org/abs/1412.1042},
    Volume = {abs/1412.1042},
    Year = {2014},
    Bdsk-Url-1 = {http://arxiv.org/abs/1412.1042}}
  • Marino Miculan. Tutorial on bigraphical reactive systems (slides). In 1st international workshop on meta models for process languages (memo), 2014.
    [Bibtex] [PDF]
    @inproceedings{miculan:memo14,
    Author = {Marino Miculan},
    Booktitle = {1st International Workshop on Meta Models for Process Languages (MeMo)},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/MeMo14-tutorial.pdf},
    Title = {Tutorial on Bigraphical Reactive Systems (slides)},
    Year = 2014}
  • Giorgio Bacci, Marino Miculan, and Romeo Rizzi. Finding a forest in a tree — the matching problem for wide reactive systems. In M. Maffei and E. Tuosto, editors, Trustworthy global computing – 9th international symposium, tgc 2014, rome, italy, september 5-6, 2014. revised selected papers, volume 8902 of Lecture Notes in Computer Science, pages 17-33. Springer, 2014.
    [Bibtex] [PDF]
    @inproceedings{bmr:tgc14,
    Author = {Giorgio Bacci and Marino Miculan and Romeo Rizzi},
    Booktitle = {Trustworthy Global Computing - 9th International Symposium, TGC 2014, Rome, Italy, September 5-6, 2014. Revised Selected Papers},
    Date-Modified = {2015-01-15 10:46:04 +0000},
    Editor = {M. Maffei and E. Tuosto},
    Pages = {17--33},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/TGC14.pdf},
    Publisher = {Springer},
    Series = lncs,
    Title = {Finding a Forest in a Tree --- The matching problem for wide reactive systems},
    Volume = {8902},
    Year = 2014}
  • A. Bizjak, Lars Birkedal, and Marino Miculan. A model of countable nondeterminism in guarded type theory. In Gilles Dowek, editor, Proc. rta-tlca, volume 8560 of Lecture Notes in Computer Science, pages 108-123. Springer, 2014.
    [Bibtex] [PDF]
    @inproceedings{bbm:tlca14,
    Author = {A. Bizjak and Lars Birkedal and Marino Miculan},
    Booktitle = {Proc. RTA-TLCA},
    Date-Modified = {2015-01-15 12:12:02 +0000},
    Editor = {Gilles Dowek},
    Pages = {108-123},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/TLCA14.pdf},
    Publisher = {Springer},
    Series = lncs,
    Title = {A Model of Countable Nondeterminism in Guarded Type Theory},
    Volume = {8560},
    Year = 2014}
  • Alessio Mansutti, Marino Miculan, and Marco Peressotti. Multi-agent systems design and prototyping with bigraphical reactive systems. In K. Magoutis and P. Pietzuch, editors, Proc. dais 2014, number 8460 in Lecture Notes in Computer Science, pages 201-208, 2014.
    [Bibtex] [PDF]
    @inproceedings{mmp:dais14,
    Author = {Alessio Mansutti and Marino Miculan and Marco Peressotti},
    Booktitle = {Proc. DAIS 2014},
    Editor = {K. Magoutis and P. Pietzuch},
    Number = 8460,
    Pages = {201--208},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/DAIS14.pdf},
    Series = lncs,
    Title = {Multi-agent Systems Design and Prototyping with Bigraphical Reactive Systems},
    Year = 2014}
  • Furio Honsell, Luigi Liquori, and Ivan Scagnetto. LaxF: side conditions and external evidence as monads. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, Mathematical foundations of computer science 2014, volume 8634 of Lecture Notes in Computer Science, pages 327-339. Springer Berlin Heidelberg, 2014.
    [Bibtex] [DOI] [url]
    @incollection{hls:mfcs14,
    year={2014},
    isbn={978-3-662-44521-1},
    booktitle={Mathematical Foundations of Computer Science 2014},
    volume={8634},
    series={Lecture Notes in Computer Science},
    editor={Csuhaj-Varjú, Erzsébet and Dietzfelbinger, Martin and Ésik, Zoltán},
    doi={10.1007/978-3-662-44522-8_28},
    title={{LaxF}: Side Conditions and External Evidence as Monads},
    url={http://dx.doi.org/10.1007/978-3-662-44522-8_28},
    publisher={Springer Berlin Heidelberg},
    author={Honsell, Furio and Liquori, Luigi and Scagnetto, Ivan},
    pages={327-339},
    language={English}
    }
  • Alberto Ciaffaglione and Ivan Scagnetto. Internal adequacy of bookkeeping in coq. In Proceedings of the 2014 international workshop on logical frameworks and meta-languages: theory and practice, LFMTP ’14, pages 8:1–8:8, New York, NY, USA, 2014. ACM.
    [Bibtex] [DOI] [url]
    @inproceedings{Ciaffaglione:2014:IAB:2631172.2631180,
    author = {Ciaffaglione, Alberto and Scagnetto, Ivan},
    title = {Internal Adequacy of Bookkeeping in Coq},
    booktitle = {Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice},
    series = {LFMTP '14},
    year = {2014},
    isbn = {978-1-4503-2817-3},
    location = {Vienna, Austria},
    pages = {8:1--8:8},
    articleno = {8},
    numpages = {8},
    url = {http://doi.acm.org/10.1145/2631172.2631180},
    doi = {10.1145/2631172.2631180},
    acmid = {2631180},
    publisher = {ACM},
    address = {New York, NY, USA},
    keywords = {Higher-Order Abstract Syntax, Logical Frameworks, Type Theory},
    }
  • Stefano Mizzaro, Marco Pavan, Ivan Scagnetto, and Martino Valenti. Short text categorization exploiting contextual enrichment and external knowledge. In Proceedings of the first international workshop on social media retrieval and analysis, SoMeRA ’14, pages 57-62, New York, NY, USA, 2014. ACM.
    [Bibtex] [DOI] [url]
    @inproceedings{Mizzaro:2014:STC:2632188.2632205,
    author = {Mizzaro, Stefano and Pavan, Marco and Scagnetto, Ivan and Valenti, Martino},
    title = {Short Text Categorization Exploiting Contextual Enrichment and External Knowledge},
    booktitle = {Proceedings of the First International Workshop on Social Media Retrieval and Analysis},
    series = {SoMeRA '14},
    year = {2014},
    isbn = {978-1-4503-3022-0},
    location = {Gold Coast, Queensland, Australia},
    pages = {57--62},
    numpages = {6},
    url = {http://doi.acm.org/10.1145/2632188.2632205},
    doi = {10.1145/2632188.2632205},
    acmid = {2632205},
    publisher = {ACM},
    address = {New York, NY, USA},
    keywords = {context-aware retrieval, enrichment, evaluation, wikipedia},
    }
  • Stefano Mizzaro, Marco Pavan, Ivan Scagnetto, and Ivano Zanello. A context-aware retrieval system for mobile applications. In Proceedings of the 4th workshop on context-awareness in retrieval and recommendation, CARR ’14, pages 18-25, New York, NY, USA, 2014. ACM.
    [Bibtex] [DOI] [url]
    @inproceedings{Mizzaro:2014:CRS:2601301.2601305,
    author = {Mizzaro, Stefano and Pavan, Marco and Scagnetto, Ivan and Zanello, Ivano},
    title = {A Context-aware Retrieval System for Mobile Applications},
    booktitle = {Proceedings of the 4th Workshop on Context-Awareness in Retrieval and Recommendation},
    series = {CARR '14},
    year = {2014},
    isbn = {978-1-4503-2723-7},
    location = {Amsterdam, The Netherlands},
    pages = {18--25},
    numpages = {8},
    url = {http://doi.acm.org/10.1145/2601301.2601305},
    doi = {10.1145/2601301.2601305},
    acmid = {2601305},
    publisher = {ACM},
    address = {New York, NY, USA},
    keywords = {apps, context-aware retrieval, evaluation, mobile, ranking, recommender systems},
    }

2013

  • Marino Miculan and Marco Peressotti. Bigraphs reloaded. Technical Report UDMI/01/2013/RR, Dept. of Mathematics and Computer Science, Univ. of Udine, 2013.
    [Bibtex] [PDF]
    @techreport{mp:br-tr,
    Author = {Marino Miculan and Marco Peressotti},
    Institution = {Dept. of Mathematics and Computer Science, Univ. of Udine},
    Number = {UDMI/01/2013/RR},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/UDMI012013.pdf},
    Title = {Bigraphs Reloaded},
    Year = 2013}
  • Marino Miculan and Marco Peressotti. Weak bisimulations for labelled transition systems weighted over semirings. Corr, abs/1310.4106, 2013.
    [Bibtex] [url]
    @article{mp:wblts-tr,
    Author = {Marino Miculan and Marco Peressotti},
    Bibsource = {DBLP, http://dblp.uni-trier.de},
    Journal = {CoRR},
    Title = {Weak bisimulations for labelled transition systems weighted over semirings},
    Url = {http://arxiv.org/abs/1310.4106},
    Volume = {abs/1310.4106},
    Year = {2013},
    Bdsk-Url-1 = {http://arxiv.org/abs/1310.4106}}
  • Furio Honsell, Marina Lenisa, Ivan Scagnetto, Luigi Liquori, and Petar Maksimovic. An open logical framework. Journal of logic and computation, 2013.
    [Bibtex] [DOI] [url]
    @article{Honsell31072013,
    author = {Honsell, Furio and Lenisa, Marina and Scagnetto, Ivan and Liquori, Luigi and Maksimovic, Petar},
    title = {An open logical framework},
    year = {2013},
    doi = {10.1093/logcom/ext028},
    abstract ={The LFP Framework is an extension of the Harper–Honsell–Plotkin's Edinburgh Logical Framework LF with external predicates, hence the name Open Logical Framework. This is accomplished by defining lock type constructors, which are a sort of ⋄-modality constructors, releasing their argument under the condition that a possibly external predicate is satisfied on an appropriate typed judgement. Lock types are defined using the standard pattern of constructive type theory, i.e. via introduction, elimination and equality rules. Using LFP , one can factor out the complexity of encoding specific features of logical systems, which would otherwise be awkwardly encoded in LF, e.g. side-conditions in the application of rules in Modal Logics, and sub-structural rules, as in non-commutative Linear Logic. The idea of LFP is that these conditions need only to be specified, while their verification can be delegated to an external proof engine, in the style of the Poincaré Principle or Deduction Modulo. Indeed such paradigms can be adequately formalized in LFP . We investigate and characterize the meta-theoretical properties of the calculus underpinning LFP : strong normalization, confluence and subject reduction. This latter property holds under the assumption that the predicates are well-behaved, i.e. closed under weakening, permutation, substitution and reduction in the arguments. Moreover, we provide a canonical presentation of LFP , based on a suitable extension of the notion of βη-long normal form, allowing for smooth formulations of adequacy statements.},
    URL = {http://logcom.oxfordjournals.org/content/early/2013/07/31/logcom.ext028.abstract},
    eprint = {http://logcom.oxfordjournals.org/content/early/2013/07/31/logcom.ext028.full.pdf+html},
    journal = {Journal of Logic and Computation}
    }

2012

  • Marino Miculan and Marco Paviotti. Synthesis of distributed mobile programs using monadic types in coq. In Lennart Beringer and Amy P. Felty, editors, Interactive theorem proving – third international conference, ITP 2012, princeton, nj, usa, august 13-15, 2012. proceedings, volume 7406 of Lecture Notes in Computer Science, pages 183-200. Springer, 2012.
    [Bibtex] [PDF] [DOI] [url]
    @inproceedings{mp:itp12,
    Author = {Marino Miculan and Marco Paviotti},
    Bibsource = {dblp computer science bibliography, http://dblp.org},
    Biburl = {http://dblp.uni-trier.de/rec/bib/conf/itp/MiculanP12},
    Booktitle = {Interactive Theorem Proving - Third International Conference, {ITP} 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings},
    Date-Added = {2015-01-15 11:46:28 +0000},
    Date-Modified = {2015-01-15 11:48:54 +0000},
    Doi = {10.1007/978-3-642-32347-8_13},
    Editor = {Lennart Beringer and Amy P. Felty},
    Pages = {183--200},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/ITP12.pdf},
    Publisher = {Springer},
    Series = {Lecture Notes in Computer Science},
    Timestamp = {Tue, 14 Aug 2012 11:20:26 +0200},
    Title = {Synthesis of Distributed Mobile Programs Using Monadic Types in Coq},
    Url = {http://dx.doi.org/10.1007/978-3-642-32347-8_13},
    Volume = {7406},
    Web = {http://users.dimi.uniud.it/~marino.miculan/wordpress/downloads/erlang-coq-synthesizer},
    Year = {2012},
    Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-642-32347-8_13}}
  • Marino Miculan and Ilaria Sambarino. Implementing the stochastics brane calculus in a generic stochastic abstract machine. In Gabriel Ciobanu, editor, Proceedings 6th workshop on membrane computing and biologically inspired process calculi, newcastle, uk, 8th september 2012, volume 100 of Electronic Proceedings in Theoretical Computer Science, pages 82-100. Open Publishing Association, 2012.
    [Bibtex] [PDF] [DOI] [url]
    @inproceedings{EPTCS100.6,
    Author = {Miculan, Marino and Sambarino, Ilaria},
    Booktitle = {Proceedings 6th Workshop on Membrane Computing and Biologically Inspired Process Calculi, Newcastle, UK, 8th September 2012},
    Doi = {10.4204/EPTCS.100.6},
    Editor = {Ciobanu, Gabriel},
    Pages = {82-100},
    Pdf = {http://arxiv.org/pdf/1211.4094v1},
    Publisher = {Open Publishing Association},
    Series = {Electronic Proceedings in Theoretical Computer Science},
    Title = {Implementing the Stochastics Brane Calculus in a Generic Stochastic Abstract Machine},
    Url = {http://dx.doi.org/10.4204/EPTCS.100.6},
    Volume = {100},
    Year = {2012},
    Bdsk-Url-1 = {http://dx.doi.org/10.4204/EPTCS.100.6}}
  • Giorgio Bacci and Marino Miculan. Measurable stochastics for Brane Calculus. Theoretical computer science, 431:117-136, 2012.
    [Bibtex] [PDF] [DOI] [url]
    @article{bm:tcs12,
    Author = {Giorgio Bacci and Marino Miculan},
    Doi = {10.1016/j.tcs.2011.12.055},
    Issn = {0304-3975},
    Journal = {Theoretical Computer Science},
    Pages = {117--136},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/TCS12.pdf},
    Title = {Measurable Stochastics for {Brane Calculus}},
    Url = {http://dx.doi.org/10.1016/j.tcs.2011.12.055},
    Volume = 431,
    Year = 2012,
    Bdsk-Url-1 = {http://dx.doi.org/10.1016/j.tcs.2011.12.055}}
  • Giorgio Bacci and Marino Miculan. Structural operational semantics for continuous state probabilistic processes. In Proc. cmcs’12, volume 7399 of Lecture Notes in Computer Science, pages 71-90. Springer, 2012.
    [Bibtex] [PDF]
    @inproceedings{bm:cmcs12,
    Author = {Giorgio Bacci and Marino Miculan},
    Booktitle = {Proc. CMCS'12},
    Pages = {71-90},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/CMCS12.pdf},
    Publisher = {Springer},
    Series = LNCS,
    Title = {Structural operational semantics for continuous state probabilistic processes},
    Volume = 7399,
    Year = 2012}
  • Alberto Ciaffaglione and Ivan Scagnetto. A weak HOAS approach to the poplmark challenge. In Proceedings seventh workshop on logical and semantic frameworks, with applications, LSFA 2012, rio de janeiro, brazil, september 29-30, 2012., pages 109-124, 2012.
    [Bibtex] [DOI] [url]
    @inproceedings{DBLP:journals/corr/abs-1303-7332,
    author = {Alberto Ciaffaglione and
    Ivan Scagnetto},
    title = {A weak {HOAS} approach to the POPLmark Challenge},
    booktitle = {Proceedings Seventh Workshop on Logical and Semantic Frameworks, with
    Applications, {LSFA} 2012, Rio de Janeiro, Brazil, September 29-30,
    2012.},
    pages = {109--124},
    year = {2012},
    crossref = {DBLP:journals/corr/abs-1303-7136},
    url = {http://dx.doi.org/10.4204/EPTCS.113.11},
    doi = {10.4204/EPTCS.113.11},
    timestamp = {Sun, 15 Mar 2015 09:37:18 +0100},
    biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1303-7332},
    bibsource = {dblp computer science bibliography, http://dblp.org}
    }
  • Furio Honsell, Marina Lenisa, Luigi Liquori, Petar Maksimovic, and Ivan Scagnetto. Lfp: a logical framework with external predicates. In Proceedings of the seventh international workshop on logical frameworks and meta-languages, theory and practice, LFMTP ’12, pages 13-22, New York, NY, USA, 2012. ACM.
    [Bibtex] [DOI] [url]
    @inproceedings{Honsell:2012:LPL:2364406.2364409,
    author = {Honsell, Furio and Lenisa, Marina and Liquori, Luigi and Maksimovic, Petar and Scagnetto, Ivan},
    title = {LFP: A Logical Framework with External Predicates},
    booktitle = {Proceedings of the Seventh International Workshop on Logical Frameworks and Meta-languages, Theory and Practice},
    series = {LFMTP '12},
    year = {2012},
    isbn = {978-1-4503-1578-4},
    location = {Copenhagen, Denmark},
    pages = {13--22},
    numpages = {10},
    url = {http://doi.acm.org/10.1145/2364406.2364409},
    doi = {10.1145/2364406.2364409},
    acmid = {2364409},
    publisher = {ACM},
    address = {New York, NY, USA},
    keywords = {logical frameworks, type theory},
    }

2011

  • Marino Miculan and Caterina Urban. Formal analysis of Facebook Connect single sign-on authentication protocol. In SofSem 2011, proceedings of student research forum, pages 99-116. OKAT, 2011.
    [Bibtex] [PDF]
    @inproceedings{mu:sofsem11,
    Author = {Marino Miculan and Caterina Urban},
    Booktitle = {{SofSem} 2011, Proceedings of Student Research Forum},
    Pages = {99--116},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/SOFSEM11.pdf},
    Publisher = {OKAT},
    Title = {Formal analysis of {Facebook Connect} Single Sign-On authentication protocol},
    Web = {http://users.dimi.uniud.it/~marino.miculan/Papers/fbconnect.zip},
    Year = 2011}
  • Carlo Maiero and Marino Miculan. Unobservable intrusion detection based on call traces in paravirtualized systems. In Javier Lopez and Pierangela Samarati, editors, Proc. secrypt. SciTePress, 2011.
    [Bibtex] [PDF]
    @inproceedings{mm:secrypt11,
    Author = {Carlo Maiero and Marino Miculan},
    Bibsource = {DBLP, http://dblp.uni-trier.de},
    Booktitle = {Proc. SECRYPT},
    Editor = {Javier Lopez and Pierangela Samarati},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/SECRYPT11.pdf},
    Publisher = {SciTePress},
    Title = {Unobservable Intrusion Detection Based on Call Traces in Paravirtualized Systems},
    Year = 2011}

2010

  • Davide Grohmann and Marino Miculan. Graph algebras for bigraphs. In Lara J. de C. Ermel and R. Heckel, editors, Proc. 9th international workshop on graph transformation and visual modeling techniques (gt-vmt’10), volume 10 of Electronic Communications of the EASST. European Association of Software Science and Technology, 2010.
    [Bibtex] [PDF]
    @inproceedings{gm:gtvmt10,
    Author = {Davide Grohmann and Marino Miculan},
    Booktitle = {Proc. 9th International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT'10)},
    Editor = {C. Ermel, J. de Lara and R. Heckel},
    Issn = {{ISSN 1863-2122}},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/GTVMT10.pdf},
    Publisher = {European Association of Software Science and Technology},
    Series = {Electronic Communications of the EASST},
    Title = {Graph Algebras for Bigraphs},
    Volume = 10,
    Year = 2010,
    Bdsk-Url-1 = {http://eceasst.cs.tu-berlin.de/index.php/eceasst/issue/view/19}}
  • Giorgio Bacci and Marino Miculan. Measurable stochastics for brane calculus. In Gabriel Ciobanu and Maciej Koutny, editors, Proc. mecbic, volume 40 of EPTCS, pages 6-22, 2010.
    [Bibtex] [PDF] [url]
    @inproceedings{DBLP:journals/corr/abs-1011-0488,
    Author = {Giorgio Bacci and Marino Miculan},
    Booktitle = {Proc. MeCBIC},
    Editor = {Gabriel Ciobanu and Maciej Koutny},
    Pages = {6-22},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/MeCBIC10.pdf},
    Series = {EPTCS},
    Title = {Measurable Stochastics for Brane Calculus},
    Url = {http://dx.doi.org/10.4204/EPTCS.40.2},
    Volume = 40,
    Year = 2010,
    Bdsk-Url-1 = {http://dx.doi.org/10.4204/EPTCS.40.2}}
  • Paolo Coppola, Vincenzo Della Mea, Luca Di Gaspero, Davide Menegon, Danny Mischis, Stefano Mizzaro, Ivan Scagnetto, and Luca Vassena. The context-aware browser. Intelligent systems, ieee, 25(1):38-47, 2010.
    [Bibtex]
    @article{cab2010context,
    title={The context-aware browser},
    author={Coppola, Paolo and Della Mea, Vincenzo and Di Gaspero, Luca and Menegon, Davide and Mischis, Danny and Mizzaro, Stefano and Scagnetto, Ivan and Vassena, Luca},
    journal={Intelligent Systems, IEEE},
    volume={25},
    number={1},
    pages={38--47},
    year={2010},
    publisher={IEEE}
    }
  • Paolo Coppola, Vincenzo Della Mea, Luca Di Gaspero, Raffaella Lomuscio, Danny Mischis, Stefano Mizzaro, Elena Nazzi, Ivan Scagnetto, and Luca Vassena. Ai techniques in a context-aware ubiquitous environment. In Aboul-Ella Hassanien, Jemal H. Abawajy, Ajith Abraham, and Hani Hagras, editors, Pervasive computing, Computer Communications and Networks, pages 157-180. Springer London, 2010.
    [Bibtex] [DOI] [url]
    @incollection{cab2010,
    year={2010},
    isbn={978-1-84882-598-7},
    booktitle={Pervasive Computing},
    series={Computer Communications and Networks},
    editor={Hassanien, Aboul-Ella and Abawajy, Jemal H. and Abraham, Ajith and Hagras, Hani},
    doi={10.1007/978-1-84882-599-4_8},
    title={AI Techniques in a Context-Aware Ubiquitous Environment},
    url={http://dx.doi.org/10.1007/978-1-84882-599-4_8},
    publisher={Springer London},
    keywords={Context-aware browser; CAB; MoBe; Mobile; Bayesian; Inference and wireless systems},
    author={Coppola, Paolo and Della Mea, Vincenzo and Di Gaspero, Luca and Lomuscio, Raffaella and Mischis, Danny and Mizzaro, Stefano and Nazzi, Elena and Scagnetto, Ivan and Vassena, Luca},
    pages={157-180},
    language={English}
    }

2009

  • Giorgio Bacci, Davide Grohmann, and Marino Miculan. A framework for protein and membrane interactions. In Gabriel Ciobanu, editor, Proc. mecbic’09, volume 11 of EPTCS, 2009.
    [Bibtex] [PDF]
    @inproceedings{bgm:biobeta,
    Author = {Giorgio Bacci and Davide Grohmann and Marino Miculan},
    Booktitle = {Proc. MeCBIC'09},
    Editor = {Gabriel Ciobanu},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/MeCBIC09b.pdf},
    Series = {EPTCS},
    Title = {A framework for protein and membrane interactions},
    Volume = 11,
    Year = 2009}
  • Giorgio Bacci, Davide Grohmann, and Marino Miculan. Bigraphical models for protein and membrane interactions. In Gabriel Ciobanu, editor, Proc. mecbic’09, volume 11 of EPTCS, 2009.
    [Bibtex] [PDF]
    @inproceedings{bgm:biobig,
    Author = {Giorgio Bacci and Davide Grohmann and Marino Miculan},
    Booktitle = {Proc. MeCBIC'09},
    Editor = {Gabriel Ciobanu},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/MeCBIC09a.pdf},
    Series = {EPTCS},
    Title = {Bigraphical models for protein and membrane interactions},
    Volume = 11,
    Year = 2009}
  • Giorgio Bacci, Davide Grohmann, and Marino Miculan. Dbtk: a toolkit for directed bigraphs. In Calco 2009 conference proceedings – calco tools, volume 5728 of Lecture Notes in Computer Science. Springer, 2009.
    [Bibtex] [PDF] [url]
    @inproceedings{bgm:dbtk,
    Author = {Giorgio Bacci and Davide Grohmann and Marino Miculan},
    Booktitle = {CALCO 2009 Conference Proceedings - Calco Tools},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/CALCO09.pdf},
    Publisher = {Springer},
    Series = LNCS,
    Title = {DBtk: a Toolkit for Directed Bigraphs},
    Url = {http://users.dimi.uniud.it/~davide.grohmann/dbtk/},
    Volume = 5728,
    Year = 2009,
    Bdsk-Url-1 = {http://users.dimi.uniud.it/~davide.grohmann/dbtk/}}
  • Davide Grohmann and Marino Miculan. Deriving barbed bisimulations for bigraphical reactive systems. In A. Corradini and E. Tuosto, editors, Proceedings of international conference on graph transformation (icgt-ds 2008), volume 16 of Electronic Communications of the EASST. European Association of Software Science and Technology, 2009.
    [Bibtex] [PDF]
    @inproceedings{gm:icgt-ds08,
    Author = {Davide Grohmann and Marino Miculan},
    Booktitle = {Proceedings of International Conference on Graph Transformation (ICGT-DS 2008)},
    Editor = {A. Corradini and E. Tuosto},
    Issn = {{ISSN 1863-2122}},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/ICGT08-DS.pdf},
    Publisher = {European Association of Software Science and Technology},
    Series = {Electronic Communications of the EASST},
    Title = {Deriving Barbed Bisimulations for Bigraphical Reactive Systems},
    Volume = 16,
    Year = 2009,
    Bdsk-Url-1 = {http://eceasst.cs.tu-berlin.de/index.php/eceasst/issue/view/19}}

2008

  • Marino Miculan. A categorical model of the Fusion calculus. In Proc. xxiv mfps, volume 218 of Electronic Notes in Theoretical Computer Science, pages 275-293. Elsevier, 2008.
    [Bibtex] [PDF]
    @inproceedings{miculan:mfps08,
    Author = {Marino Miculan},
    Booktitle = {Proc. XXIV MFPS},
    Pages = {275-293},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/MFPS08.pdf},
    Publisher = {Elsevier},
    Series = ENTCS,
    Title = {A categorical model of the {Fusion} calculus},
    Volume = 218,
    Year = 2008}
  • Davide Grohmann and Marino Miculan. An algebra for directed bigraphs. Electronic notes in theoretical computer science, 203(1):49-63, 2008.
    [Bibtex] [PDF] [DOI]
    @article{gm:termgraph07,
    Author = {Davide Grohmann and Marino Miculan},
    Booktitle = {Proceedings of TERMGRAPH 2007},
    Date-Modified = {2015-01-15 11:52:22 +0000},
    Doi = {10.1016/j.entcs.2008.03.033},
    Editor = {Ian Mackie and Detlef Plump},
    Journal = {Electronic Notes in Theoretical Computer Science},
    Number = 1,
    Pages = {49--63},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/TERMGRAPH07.pdf},
    Publisher = {Elsevier},
    Title = {An Algebra for Directed Bigraphs},
    Volume = 203,
    Year = 2008,
    Bdsk-Url-1 = {http://dx.doi.org/10.1016/j.entcs.2008.03.033}}
  • Davide Grohmann and Marino Miculan. Controlling resource access in directed bigraphs (long version). In Lara J. de C. Ermel and R. Heckel, editors, Proc. 7th international workshop on graph transformation and visual modeling techniques (gt-vmt’08), volume 10 of Electronic Communications of the EASST. European Association of Software Science and Technology, 2008.
    [Bibtex] [PDF]
    @inproceedings{gm:gtvmt08,
    Author = {Davide Grohmann and Marino Miculan},
    Booktitle = {Proc. 7th International Workshop on Graph Transformation and Visual Modeling Techniques (GT-VMT'08)},
    Editor = {C. Ermel, J. de Lara and R. Heckel},
    Issn = {1863-2122},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/GTVMT08-long.pdf},
    Publisher = {European Association of Software Science and Technology},
    Series = {Electronic Communications of the EASST},
    Title = {Controlling resource access in Directed Bigraphs (long version)},
    Volume = 10,
    Year = 2008}
  • Temesghen Kahsai and Marino Miculan. Implementing spi-calculus using nominal techniques. In Arnold Beckmann, Costas Dimitracopoulos, and Benedikt Löwe, editors, Proc. computability in europe (cie), volume 5028 of Lecture Notes in Computer Science, pages 294-305. Springer, 2008.
    [Bibtex] [PDF]
    @inproceedings{km:cie08,
    Author = {Temesghen Kahsai and Marino Miculan},
    Booktitle = {Proc. Computability in Europe (CiE)},
    Editor = {Arnold Beckmann and Costas Dimitracopoulos and Benedikt L{\"o}we},
    Isbn = {978-3-540-69405-2},
    Pages = {294-305},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/CIE08.pdf},
    Publisher = {Springer},
    Series = LNCS,
    Title = {Implementing Spi-Calculus Using Nominal Techniques},
    Volume = 5028,
    Year = 2008}
  • Silvia Crafa, Matteo Mio, Marino Miculan, Carla Piazza, and Sabina Rossi. Picnic — pi-calculus non-interference checker. In Jonathan Billington, Zhenhua Duan, and Maceij Koutny, editors, Proc. acsd’08, pages 33-38. IEEE, 2008.
    [Bibtex] [PDF] [url]
    @inproceedings{cmmpr08,
    Author = {Silvia Crafa and Matteo Mio and Marino Miculan and Carla Piazza and Sabina Rossi},
    Booktitle = {Proc. ACSD'08},
    Editor = {Jonathan Billington and Zhenhua Duan and Maceij Koutny},
    Pages = {33--38},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/ACSD08.pdf},
    Publisher = {IEEE},
    Title = {PicNIc -- Pi-calculus Non-Interference checker},
    Url = {https://sites.google.com/site/miomatteo/Home/picnic},
    Year = 2008,
    Bdsk-Url-1 = {https://sites.google.com/site/miomatteo/Home/picnic}}
  • Marino Miculan, Ivan Scagnetto, and Furio Honsell, editors. Types for proofs and programs, international conference, types 2007, cividale del friuli, italy, may 2-5, 2007, revised selected papers, volume 4941 of Lecture Notes in Computer ScienceSpringer, 2008.
    [Bibtex] [url]
    @proceedings{types07,
    Author = {Marino Miculan and Ivan Scagnetto and Furio Honsell},
    Bibsource = {DBLP, http://dblp.uni-trier.de},
    Booktitle = {Proc. TYPES},
    Date-Modified = {2015-01-15 12:23:10 +0000},
    Editor = {Marino Miculan and Ivan Scagnetto and Furio Honsell},
    Isbn = {978-3-540-68084-0},
    Publisher = {Springer},
    Series = LNCS,
    Title = {Types for Proofs and Programs, International Conference, TYPES 2007, Cividale del Friuli, Italy, May 2-5, 2007, Revised Selected Papers},
    Url = {http://dx.doi.org/10.1007/978-3-540-68103-8},
    Volume = 4941,
    Year = 2008,
    Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-540-68103-8}}
  • Giorgio Bacci and Marino Miculan. Undecidability of model checking in brane logic. Electronic notes in theoretical computer science, 192(3), 2008.
    [Bibtex] [PDF]
    @article{bm:dcm07,
    Author = {Giorgio Bacci and Marino Miculan},
    Booktitle = {Proc. 3rd Int. Workshop on Development of Computational Models, DCM'07},
    Date-Modified = {2015-01-15 11:51:25 +0000},
    Journal = {Electronic Notes in Theoretical Computer Science},
    Number = 3,
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/DCM07.pdf},
    Publisher = {Elsevier},
    Title = {Undecidability of Model checking in Brane Logic},
    Volume = 192,
    Year = 2008}
  • Adolfo Bulfoni, Coppola Coppola, Vincenzo Della Mea, Luca Di Gaspero, Danny Mischis, Stefano Mizzaro, Ivan Scagnetto, and Luca Vassena. Ai on the move: exploiting ai techniques for context inference on mobile devices. In Proceedings of the 18th european conference on artificial intelligence (ecai 2008), pages 668-672, Amsterdam — NLD, 21-25/07/ 2008. IOS Press.
    [Bibtex]
    @inproceedings{ecai2008,
    address={Amsterdam -- NLD},
    author={Bulfoni, Adolfo and Coppola, Coppola and Della Mea, Vincenzo and Di Gaspero, Luca and Mischis, Danny and Mizzaro, Stefano and Scagnetto, Ivan and Vassena, Luca},
    booktitle={Proceedings of the 18th European Conference on Artificial Intelligence (ECAI 2008)},
    location={Patras, Greece},
    month={21-25/07/},
    pages={668--672},
    publisher={IOS Press},
    title={AI on the Move: Exploiting AI Techniques for Context Inference on Mobile Devices},
    year={2008}
    }

2007

  • Davide Grohmann and Marino Miculan. Directed bigraphs. In Proc. xxiii mfps, volume 173 of Electronic Notes in Theoretical Computer Science, pages 121-137. Elsevier, 2007.
    [Bibtex] [PDF]
    @inproceedings{gm:mfps07,
    Author = {Davide Grohmann and Marino Miculan},
    Booktitle = {Proc. XXIII MFPS},
    Pages = {121--137},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/MFPS07.pdf},
    Publisher = {Elsevier},
    Series = ENTCS,
    Title = {Directed bigraphs},
    Volume = 173,
    Year = 2007}
  • Davide Grohmann and Marino Miculan. Reactive systems over directed bigraphs. In Luis Caires and Vasco Vasconcelos, editors, Proc. concur 2007, volume 4703 of Lecture Notes in Computer Science, pages 380-394. Springer, 2007.
    [Bibtex] [PDF]
    @inproceedings{gm:concur07,
    Author = {Davide Grohmann and Marino Miculan},
    Booktitle = {Proc. CONCUR 2007},
    Editor = {Luis Caires and Vasco Vasconcelos},
    Isbn = {978-3-540-74406-1},
    Pages = {380--394},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/CONCUR07.pdf},
    Publisher = {Springer},
    Series = {Lecture Notes in Computer Science},
    Title = {Reactive Systems over Directed Bigraphs},
    Volume = 4703,
    Year = 2007}
  • Alberto Ciaffaglione, Luigi Liquori, and Marino Miculan. Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts. J. autom. reasoning, 39(1):1-47, 2007.
    [Bibtex] [PDF]
    @article{CLM07,
    Author = {Alberto Ciaffaglione and Luigi Liquori and Marino Miculan},
    Bibsource = {DBLP, http://dblp.uni-trier.de},
    Ee = {http://dx.doi.org/10.1007/s10817-006-9061-y},
    Journal = {J. Autom. Reasoning},
    Number = 1,
    Pages = {1-47},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/JAR07.pdf},
    Title = {Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts},
    Volume = 39,
    Year = 2007}

2006

  • Davide Grohmann and Marino Miculan. Directed bigraphs: theory and applications. Technical Report UDMI/12/2006/RR, Department of Mathematics and Computer Science, University of Udine, 2006. Available at \url{http://www.dimi.uniud.it/miculan/Papers/}.
    [Bibtex] [PDF]
    @techreport{gm:tr06,
    Author = {Davide Grohmann and Marino Miculan},
    Institution = {Department of Mathematics and Computer Science, University of Udine},
    Note = {Available at \url{http://www.dimi.uniud.it/miculan/Papers/}.},
    Number = {UDMI/12/2006/RR},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/UDMI122006.pdf},
    Title = {Directed bigraphs: theory and applications},
    Year = 2006}
  • Marino Miculan and Giorgio Bacci. Modal logics for brane calculus. In Corrado Priami, editor, Proc. cmsb, volume 4210 of Lecture Notes in Computer Science, pages 1-16. Springer, 2006.
    [Bibtex] [PDF]
    @inproceedings{mb:cmsb06,
    Author = {Marino Miculan and Giorgio Bacci},
    Bibsource = {DBLP, http://dblp.uni-trier.de},
    Booktitle = {Proc. CMSB},
    Editor = {Corrado Priami},
    Isbn = {3-540-46166-3},
    Pages = {1-16},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/MeCBIC10.pdf},
    Publisher = {Springer},
    Series = LNCS,
    Title = {Modal Logics for Brane Calculus},
    Volume = 4210,
    Year = 2006}

2005

  • Maja Massarini, Marino Miculan, and Francesco Sepic. Implementazione di memoria distribuita su cluster compactpci. In Atti del congresso aica 2005. AICA,, 2005.
    [Bibtex] [PDF]
    @inproceedings{mms:aica05,
    Author = {Maja Massarini and Marino Miculan and Francesco Sepic},
    Booktitle = {Atti del Congresso AICA 2005},
    Organization = {AICA},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/AICA05.pdf},
    Title = {Implementazione di Memoria Distribuita su cluster CompactPCI},
    Year = 2005}
  • Paolo Coppola, Vincenzo Della Mea, Luca Di Gaspero, Stefano Mizzaro, Ivan Scagnetto, Andrea Selva, Luca Vassena, and Paolo Zandegiacomo Riziò. Mobe: a framework for context-aware mobile applications. In Proc. of workshop on context awareness for proactive systems (caps2005), page –, Helsinki — FIN, 2005. Helsinki University Press.
    [Bibtex]
    @inproceedings{caps2005,
    address={Helsinki -- FIN},
    author={Coppola, Paolo and Della Mea, Vincenzo and Di Gaspero, Luca and Mizzaro, Stefano and Scagnetto, Ivan and Selva, Andrea and Vassena, Luca and Zandegiacomo Rizi\`o, Paolo},
    booktitle={Proc. of Workshop on Context Awareness for Proactive Systems (CAPS2005)},
    pages={--},
    publisher={Helsinki University Press},
    title={MoBe: a framework for context-aware mobile applications},
    year=2005,
    }
  • Paolo Coppola, Vincenzo Della Mea, Luca Di Gaspero, Stefano Mizzaro, Ivan Scagnetto, Andrea Selva, Luca Vassena, and Paolo Zandegiacomo Riziò. Mobe: context-aware mobile applications on mobile devices for mobile users. In Proc. of 1st int. workshop on exploiting context histories in smart environments (echise2005), page –, 2005.
    [Bibtex]
    @inproceedings{echise2005,
    author={Coppola, Paolo and Della Mea, Vincenzo and Di Gaspero, Luca and Mizzaro, Stefano and Scagnetto, Ivan and Selva, Andrea and Vassena, Luca and Zandegiacomo Rizi\`o, Paolo},
    booktitle={Proc. of 1st Int. Workshop on Exploiting Context Histories in Smart Environments (ECHISE2005)},
    pages={--},
    title={MoBe: Context-Aware Mobile Applications on Mobile Devices for Mobile Users},
    year=2005,
    }
  • Paolo Coppola, Vincenzo Della Mea, Luca Di Gaspero, Stefano Mizzaro, Ivan Scagnetto, Andrea Selva, Luca Vassena, and Paolo Zandegiacomo Riziò. Information filtering and retrieving of context-aware applications within the mobe framework. In International workshop on context-based information retrieval (cir-05), page –, 2005.
    [Bibtex]
    @inproceedings{cir2005,
    author={Coppola, Paolo and Della Mea, Vincenzo and Di Gaspero, Luca and Mizzaro, Stefano and Scagnetto, Ivan and Selva, Andrea and Vassena, Luca and Zandegiacomo Rizi\`o, Paolo},
    booktitle={International Workshop on Context-Based Information Retrieval (CIR-05)},
    pages={--},
    title={Information Filtering and Retrieving of Context-Aware Applications within the MoBe Framework},
    year=2005,
    }

2004

  • Roberto Bruni, Furio Honsell, Marina Lenisa, and Marino Miculan. Modeling fresh names in π-calculus using abstractions. In Jiri Adamek, editor, Proc. cmcs’04, volume 106 of Electronic Notes in Theoretical Computer Science. Elsevier, 2004.
    [Bibtex] [PDF]
    @inproceedings{bhlm:cmcs04,
    Author = {Roberto Bruni and Furio Honsell and Marina Lenisa and Marino Miculan},
    Booktitle = {Proc. CMCS'04},
    Editor = {Jiri Adamek},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/CMCS04.pdf},
    Publisher = {Elsevier},
    Series = ENTCS,
    Title = {Modeling Fresh Names in π-calculus Using Abstractions},
    Volume = 106,
    Year = 2004}
  • Furio Honsell and Ivan Scagnetto. Mobility types in coq. In Stefano Berardi, Mario Coppo, and Ferruccio Damiani, editors, Types for proofs and programs, volume 3085 of Lecture Notes in Computer Science, pages 324-337. Springer Berlin Heidelberg, 2004.
    [Bibtex] [DOI] [url]
    @incollection{mcube2004,
    year={2004},
    isbn={978-3-540-22164-7},
    booktitle={Types for Proofs and Programs},
    volume={3085},
    series={Lecture Notes in Computer Science},
    editor={Berardi, Stefano and Coppo, Mario and Damiani, Ferruccio},
    doi={10.1007/978-3-540-24849-1_21},
    title={Mobility Types in Coq},
    url={http://dx.doi.org/10.1007/978-3-540-24849-1_21},
    publisher={Springer Berlin Heidelberg},
    author={Honsell, Furio and Scagnetto, Ivan},
    pages={324-337}
    }

2002

  • Ivan Scagnetto and Marino Miculan. Ambient calculus and its logic in the calculus of inductive constructions. In Frank Pfenning, editor, Proc. third international workshop on logical frameworks and meta-languages (lfm’02), volume 70.2 of Electronic Notes in Theoretical Computer Science. Elsevier, 2002.
    [Bibtex] [PDF]
    @inproceedings{sm02:ambients,
    Author = {Ivan Scagnetto and Marino Miculan},
    Booktitle = {Proc. Third International Workshop on Logical Frameworks and Meta-Languages (LFM'02)},
    Editor = {Frank Pfenning},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/LFM02.pdf},
    Publisher = {Elsevier},
    Series = ENTCS,
    Title = {Ambient Calculus and its Logic in the Calculus of Inductive Constructions},
    Volume = {70.2},
    Year = {2002}}

2001

  • Marino Miculan. On the formalization of the modal µ-calculus in the calculus of inductive constructions. Information and computation, 164(1):199-231, 2001.
    [Bibtex] [PDF]
    @article{mic:ic01,
    Author = {Marino Miculan},
    Date-Modified = {2015-01-15 11:37:48 +0000},
    Journal = {Information and Computation},
    Number = 1,
    Pages = {199-231},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/IC01.pdf},
    Title = {On the formalization of the modal µ-calculus in the Calculus of Inductive Constructions},
    Volume = 164,
    Year = 2001}
  • Furio Honsell, Marino Miculan, and Ivan Scagnetto. Π-calculus in (co)inductive type theory. Theoretical computer science, 253(2):239-285, 2001.
    [Bibtex] [PDF]
    @article{hms:picic,
    Author = {Furio Honsell and Marino Miculan and Ivan Scagnetto},
    Journal = {Theoretical Computer Science},
    Number = 2,
    Pages = {239-285},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/TCS99.pdf},
    Title = {π-calculus in (Co)Inductive Type Theory},
    Volume = 253,
    Year = 2001}

1998

  • Marino Miculan. A natural deduction style proof system for propositional µ-calculus and its formalization in inductive type theories. In Proc. ictcs’98. World Scientific, 1998.
    [Bibtex] [PDF]
    @inproceedings{mm:ictcs98,
    Author = {Marino Miculan},
    Booktitle = {Proc. ICTCS'98},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/ICTCS98.pdf},
    Publisher = {World Scientific},
    Title = {A Natural Deduction style proof system for propositional µ-calculus and its formalization in inductive type theories},
    Year = 1998}
  • Arnon Avron, Furio Honsell, Marino Miculan, and Cristian Paravano. Encoding modal logics in Logical Frameworks. Studia logica, 60(1):161-208, 1998.
    [Bibtex] [PDF]
    @article{ahmp:modals,
    Author = {Arnon Avron and Furio Honsell and Marino Miculan and Cristian Paravano},
    Journal = {Studia Logica},
    Number = 1,
    Pages = {161--208},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/SL98.pdf},
    Title = {Encoding Modal Logics in {L}ogical {F}rameworks},
    Volume = 60,
    Year = 1998}

1995

  • Marino Miculan and Fabio Gadducci. Modal µ-types for processes. In Dexter Kozen, editor, Proc. 10th lics, pages 221-231. IEEE Computer Society Press, 1995.
    [Bibtex] [PDF]
    @inproceedings{mg:bat,
    Author = {Marino Miculan and Fabio Gadducci},
    Booktitle = {Proc. 10th LICS},
    Editor = {Dexter Kozen},
    Pages = {221--231},
    Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/LICS95.pdf},
    Publisher = {IEEE Computer Society Press},
    Title = {Modal µ-Types for Processes},
    Year = 1995}