This page is generated automatically from this BibTeX file.

PDF files can be obtained by clicking on the red PDF icons .

Some papers have an associated webpage, with further informations (e.g. code, examples, etc.), which can be accessed by clicking on the green folder icon .

External pages (e.g. on arxiv or journals’ sites) are linked by the blue icons .

See also my pages on Google Scholar, on DBLP, and on Scopus.

### 2018

- Marco Bernardo and Marino Miculan. Constructive logical characterizations of bisimilarity for reactive probabilistic systems.
*Theoretical computer science*, 2018.

[Bibtex]`@article{Marino_Miculan51329185, title={Constructive Logical Characterizations of Bisimilarity for Reactive Probabilistic Systems}, journal={Theoretical Computer Science}, author={Marco Bernardo and Marino Miculan}, doi={10.1016/j.tcs.2018.12.003}, url={http://doi.org/10.1016/j.tcs.2018.12.003}, year=2018 }`

- Alessio Mansutti, Marino Miculan, and Marco Peressotti. Loose graph simulations. In Martina Seidl and Steffen Zschaler, editors,
*Software technologies: applications and foundations*, pages 109-126. Springer, 2018.

[Bibtex]`@InProceedings{mmp:staf17, author="Mansutti, Alessio and Miculan, Marino and Peressotti, Marco", editor="Seidl, Martina and Zschaler, Steffen", title="Loose Graph Simulations", booktitle="Software Technologies: Applications and Foundations", year="2018", publisher="Springer", pages="109--126", abstract="We introduce loose graph simulations (LGS), a new notion about labelled graphs which subsumes in an intuitive and natural way subgraph isomorphism (SGI), regular language pattern matching (RLPM) and graph simulation (GS). Being a unification of all these notions, LGS allows us to express directly also problems which are ``mixed'' instances of previous ones, and hence which would not fit easily in any of them. After the definition and some examples, we show that the problem of finding loose graph simulations is NP-complete, we provide formal translation of SGI, RLPM, and GS into LGSs, and we give the representation of a problem which extends both SGI and RLPM. Finally, we identify a subclass of the LGS problem that is polynomial.", isbn="978-3-319-74730-9", Pdf = {https://arxiv.org/pdf/1705.08241} }`

- Alessio Mansutti and Marino Miculan. Deciding hedged bisimilarity. In
*Proceedings of ICTCS 2018*, volume 2243 of*CEUR Workshop Proceedings*, pages 218-229. CEUR, 2018.

[Bibtex]`@inproceedings{DBLP:journals/corr/MansuttiMiculan18, author = {Alessio Mansutti and Marino Miculan}, title = {Deciding Hedged Bisimilarity}, url = {http://arxiv.org/abs/1611.03424}, booktitle = {Proceedings of {ICTCS} 2018}, series = {CEUR Workshop Proceedings}, volume = 2243, pages = {218--229}, publisher = {CEUR}, Pdf = {http://ceur-ws.org/Vol-2243/paper22.pdf}, year = 2018 }`

### 2017

- Marino Miculan and Marco Peressotti. Deciding weak weighted bisimulation. In
*Proceedings of ICTCS 2017*, volume 1849 of*CEUR-WS*, pages 126-137, 2017.

[Bibtex]`@inproceedings{mp:ictcs17, Author = {Marino Miculan and Marco Peressotti}, Booktitle = {Proceedings of {ICTCS} 2017}, Pdf = {http://ceur-ws.org/Vol-1949/ICTCSpaper11.pdf}, Title = {Deciding Weak Weighted Bisimulation}, series = {CEUR-WS}, Volume = 1849, pages = "126-137", Year = 2017 }`

- Marino Miculan and Marco Peressotti. Reductions for transition systems at work: deriving a logical characterization of quantitative bisimulation.
*Arxiv preprint arxiv:1704.07181*, 2017.

[Bibtex]`@article{miculan2017reductions, title={Reductions for Transition Systems at Work: Deriving a Logical Characterization of Quantitative Bisimulation}, author={Miculan, Marino and Peressotti, Marco}, journal={arXiv preprint arXiv:1704.07181}, year={2017} }`

- Marino Miculan and Florian Rabe, editors.
*LFMTP ’17: proceedings of the workshop on logical frameworks and meta-languages: theory and practice*ACM, 2017.

[Bibtex]`@proceedings{Miculan:2017:3130261, editor = {Miculan, Marino and Rabe, Florian}, title = {{LFMTP} '17: Proceedings of the Workshop on Logical Frameworks and Meta-Languages: Theory and Practice}, year = {2017}, isbn = {978-1-4503-5374-8}, location = {Oxford, United Kingdom}, publisher = {ACM}, url = "http://dl.acm.org/citation.cfm?id=3130261" }`

### 2016

- Marino Miculan and Marco Peressotti. On the bisimulation hierarchy of state-to-function transition systems. In
*Proceedings of ICTCS 2016*, volume 1720 of*CEUR-WS*, pages 88-102, 2016.

[Bibtex]`@inproceedings{mp:ictcs16, Author = {Marino Miculan and Marco Peressotti}, Booktitle = {Proceedings of {ICTCS} 2016}, Pdf = {http://ceur-ws.org/Vol-1720/full7.pdf}, Title = {On the bisimulation hierarchy of state-to-function transition systems}, series = {CEUR-WS}, Volume = 1720, pages = "88-102", Year = 2016 }`

- Marco Bernardo and Marino Miculan. Disjunctive probabilistic modal logic is enough for bisimilarity on reactive probabilistic systems. In
*Proceedings of ICTCS 2016*, volume 1720 of*CEUR-WS*, pages 203-220, 2016.

[Bibtex]`@inproceedings{bm:ictcs16, Author = {Marco Bernardo and Marino Miculan}, Booktitle = {Proceedings of {ICTCS} 2016}, Pdf = {http://ceur-ws.org/Vol-1720/full15.pdf}, Url = {https://arxiv.org/abs/1601.06198}, Title = {Disjunctive Probabilistic Modal Logic is Enough for Bisimilarity on Reactive Probabilistic Systems}, series = {CEUR-WS}, Volume = 1720, pages = "203-220", Year = 2016 }`

- Barbara Re and Marino Miculan, editors.
*Special issue on methodologies, technologies and tools enabling e-government*, volume 8 of*International Journal of Electronic Governance*, 2016.

[Bibtex]`@proceedings{rm:ijeg16, Editor = {Barbara Re and Marino Miculan}, title = "Special Issue on Methodologies, Technologies and Tools Enabling e-Government", series = "International Journal of Electronic Governance", Volume = 8, Number = 1, Url = "http://www.inderscience.com/info/inarticletoc.php?jcode=ijeg&year=2016&vol=8&issue=1", Year = 2016 }`

- Marino Miculan and Marco Peressotti. A specification of open transactional memory for Haskell.
*Corr*, abs/1602.05365, 2016.

[Bibtex]`@article{DBLP:journals/corr/MiculanP16, author = {Marino Miculan and Marco Peressotti}, title = {A Specification of Open Transactional Memory for {Haskell}}, journal = {CoRR}, volume = {abs/1602.05365}, year = {2016}, url = {http://arxiv.org/abs/1602.05365}, timestamp = {Tue, 01 Mar 2016 17:47:25 +0100}, biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/MiculanP16}, bibsource = {dblp computer science bibliography, http://dblp.org} }`

- Marino Miculan and Marco Peressotti. Structural operational semantics for non-deterministic processes with quantitative aspects.
*Theoretical computer science*, 655:135-154, 2016.

[Bibtex]`@article{mp:tcs16, title = "Structural operational semantics for non-deterministic processes with quantitative aspects", journal = "Theoretical Computer Science", volume = "655", pages = "135-154", year = "2016", issn = "0304-3975", doi = "10.1016/j.tcs.2016.01.012", url = "http://www.sciencedirect.com/science/article/pii/S0304397516000232", author = "Marino Miculan and Marco Peressotti", keywords = "Rule formats", keywords = "Behavioural congruences", keywords = "Quantitative models", abstract = "Abstract Recently, unifying theories for processes combining non-determinism with quantitative aspects (such as probabilistic or stochastically timed executions) have been proposed with the aim of providing general results and tools. This paper provides two contributions in this respect. First, we present a general \{GSOS\} specification format and a corresponding notion of bisimulation for non-deterministic processes with quantitative aspects. These specifications define labelled transition systems according to the \{ULTraS\} model, an extension of the usual \{LTSs\} where the transition relation associates any source state and transition label with state reachability weight functions (like, e.g., probability distributions). This format, hence called Weight Function \{GSOS\} (WF-GSOS), covers many known systems and their bisimulations (e.g. PEPA, TIPP, PCSP) and \{GSOS\} formats (e.g. GSOS, Weighted GSOS, Segala-GSOS). The second contribution is a characterization of these systems as coalgebras of a class of functors, parametric in the weight structure. This result allows us to prove soundness and completeness of the WF-GSOS specification format, and that bisimilarities induced by these specifications are always congruences. " }`

### 2015

- Alessio Mansutti, Marino Miculan, and Marco Peressotti. Distributed execution of bigraphical reactive systems.
*Eceasst*, 71, 2015.

[Bibtex]`@article{mmp:gcm14, author = {Alessio Mansutti and Marino Miculan and Marco Peressotti}, title = {Distributed execution of bigraphical reactive systems}, journal = {ECEASST}, volume = {71}, year = {2015}, url = {http://journal.ub.tu-berlin.de/eceasst/article/view/994}, timestamp = {Fri, 09 Oct 2015 10:03:31 +0200}, biburl = {https://dblp.org/rec/bib/journals/eceasst/MansuttiMP14}, bibsource = {dblp computer science bibliography, https://dblp.org} }`

- 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]`@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 = {10.1016/j.jcss.2014.12.003}, Issn = {0022-0000}, Journal = {Journal of Computer and System Sciences}, Keywords = {Quantitative aspects}, Title = {Structural operational semantics for continuous state stochastic transition systems}, Url = {http://www.sciencedirect.com/science/article/pii/S0022000014001652}, Year = {2015}, Volume = 81, Pages = "834-858", 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 Tom Holvoet and Mirko Viroli, editors,
*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*, volume 9037 of*Lecture Notes in Computer Science*, pages 213-229. Springer, 2015.

[Bibtex]`@inproceedings{mpt:coord15, author = {Marino Miculan and Marco Peressotti and Andrea Toneguzzo}, editor = {Tom Holvoet and Mirko Viroli}, title = {Open Transactions on Shared Memory}, 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}, series = {Lecture Notes in Computer Science}, volume = {9037}, pages = {213--229}, publisher = {Springer}, year = {2015}, url = {http://dx.doi.org/10.1007/978-3-319-19282-6_14}, doi = {10.1007/978-3-319-19282-6_14}, timestamp = {Thu, 30 Apr 2015 16:05:22 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/coordination/MiculanPT15}, bibsource = {dblp computer science bibliography, http://dblp.org} }`

- Marino Miculan, editor.
*Preproceedings of the 2nd international workshop on meta models for process languages (memo 2015)*, Grenoble, France, 2015. .

[Bibtex]`@proceedings{miculan:memo15, Address = {Grenoble, France}, Author = {Marino Miculan}, Booktitle = {PreProc. MeMo 2015}, Editor = {Marino Miculan}, Title = {PreProceedings of the 2nd International Workshop on Meta Models for Process Languages (MeMo 2015)}, Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/MeMo15-preproc.pdf}, Year = 2015}`

- Tomasz Brengos, Marino Miculan, and Marco Peressotti. Behavioural equivalences for coalgebras with unobservable moves.
*Journal of logical and algebraic methods in programming*, 84(6):826-852, 2015.

[Bibtex]`@article{bmp:jlamp15, title = "Behavioural equivalences for coalgebras with unobservable moves ", journal = "Journal of Logical and Algebraic Methods in Programming ", volume = {84}, number = {6}, pages = {826--852}, 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. " }`

### 2014

- Tomasz Brengos, Marino Miculan, and Marco Peressotti. Behavioural equivalences for coalgebras with unobservable moves.
*Corr*, abs/1411.0090, 2014.

[Bibtex]`@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]`@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}}`

- Marino Miculan and Marco Peressotti. A CSP implementation of the bigraph embedding problem.
*Corr*, abs/1412.1042, 2014.

[Bibtex]`@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]`@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]`@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]`@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]`@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}`

- Barbara Re and Marino Miculan, editors.
*Metteg14, proceedings of the 8th international conference on methodologies, technologies and tools enabling e-government*, Italy, 2014. Universitas Studiorum.

[Bibtex]`@proceedings{rm:metteg14, Address = {Italy}, Author = {Barbara Re and Marino Miculan}, Booktitle = {Proc. MeTTeG14}, Date-Modified = {2015-01-15 11:55:59 +0000}, Editor = {Barbara Re and Marino Miculan}, Publisher = {Universitas Studiorum}, Title = {MeTTeG14, Proceedings of the 8th International Conference on Methodologies, Technologies and Tools Enabling e-Government}, Year = 2014}`

### 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]`@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]`@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}}`

### 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]`@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]`@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]`@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]`@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}`

### 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]`@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]`@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]`@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]`@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}}`

- Karl Crary and Marino Miculan, editors.
*Proceedings 5th international workshop on logical frameworks and meta-languages: theory and practice*, volume 34 of*EPTCS*, 2010.

[Bibtex]`@proceedings{lfmtp10, Author = {Karl Crary and Marino Miculan}, Bibsource = {DBLP, http://dblp.uni-trier.de}, Booktitle = {Proc. LFMTP}, Date-Modified = {2015-01-15 11:57:26 +0000}, Editor = {Karl Crary and Marino Miculan}, Series = {EPTCS}, Title = {Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice}, Volume = 34, Year = 2010}`

### 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]`@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]`@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]`@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]`@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]`@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]`@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]`@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]`@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]`@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 Science*Springer, 2008.

[Bibtex]`@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]`@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}`

### 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]`@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]`@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]`@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

- Anna Bucalo, Martin Hofmann, Furio Honsell, Marino Miculan, and Ivan Scagnetto. Consistency of the theory of contexts.
*Journal of functional programming*, 16(3):327-395, 2006.

[Bibtex]`@article{bhhms, Author = {Anna Bucalo and Martin Hofmann and Furio Honsell and Marino Miculan and Ivan Scagnetto}, Journal = {Journal of Functional Programming}, Month = may, Number = 3, Pages = {327-395}, Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/JFP05.pdf}, Title = {Consistency of the Theory of Contexts}, Volume = 16, Year = 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]`@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]`@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}`

- Fabio Gadducci, Marino Miculan, and Ugo Montanari. On permutation algebras, (pre)sheaves and named sets.
*Higher-order and symbolic computation*, 19(2-3):283-304, 2006.

[Bibtex]`@article{gmm:hosc05, Author = {Fabio Gadducci and Marino Miculan and Ugo Montanari}, Journal = {Higher-Order and Symbolic Computation}, Month = sep, Number = {2-3}, Pages = {283-304}, Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/HOSC06.pdf}, Title = {On permutation algebras, (pre)sheaves and named sets}, Volume = 19, Year = 2006}`

### 2005

- Marino Miculan and Kidane Yemane. A unifying model of variables and names. In Vladimiro Sassone, editor,
*Proc. fossacs’05*, volume 3441 of*Lecture Notes in Computer Science*, pages 170-186, 2005.

[Bibtex]`@inproceedings{my:fossacs05, Author = {Marino Miculan and Kidane Yemane}, Booktitle = {Proc. FOSSACS'05}, Editor = {Vladimiro Sassone}, Month = apr, Pages = {170-186}, Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/FOSSACS05.pdf}, Series = LNCS, Title = {A unifying model of variables and names}, Volume = 3441, Year = 2005}`

- Maja Massarini, Marino Miculan, and Francesco Sepic. Implementazione di memoria distribuita su cluster compactpci. In
*Atti del congresso aica 2005*. AICA,, 2005.

[Bibtex]`@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}`

### 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]`@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, Marina Lenisa, and Marino Miculan, editors.
*Proceedings of the workshop of the cometa project on computational metamodels*, volume 104 of*ENTCS*Elsevier, 2004.

[Bibtex]`@proceedings{cometa03, Author = {Furio Honsell and Marina Lenisa and Marino Miculan}, Booktitle = {Proc. COMETA'03}, Date-Modified = {2015-01-15 12:24:17 +0000}, Editor = {Furio Honsell and Marina Lenisa and Marino Miculan}, Publisher = {Elsevier}, Series = {ENTCS}, Title = {Proceedings of the Workshop of the COMETA Project on Computational Metamodels}, Url = {http://www.sciencedirect.com/science/journal/15710661/104}, Volume = 104, Year = 2004, Bdsk-Url-1 = {http://www.sciencedirect.com/science/journal/15710661/104}}`

- Pietro Di Gianantonio and Marino Miculan. Unifying recursive and co-recursive definitions in sheaf categories. In Igor Walukiewicz, editor,
*Proc. fossacs’04*, volume 2987 of*Lecture Notes in Computer Science*, pages 136-150. Springer, 2004.

[Bibtex]`@inproceedings{dgm:fossacs04, Author = {Di Gianantonio, Pietro and Marino Miculan}, Booktitle = {Proc. FOSSACS'04}, Editor = {Igor Walukiewicz}, Pages = {136-150}, Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/FOSSACS04.pdf}, Publisher = {Springer}, Series = LNCS, Title = {Unifying Recursive and Co-recursive Definitions in Sheaf Categories}, Volume = 2987, Year = 2004}`

### 2003

- Marino Miculan and Ivan Scagnetto. A framework for typed HOAS and semantics. In Dale Miller, editor,
*Proc. ppdp’03*, pages 184-194. ACM Press, 2003.

[Bibtex]`@inproceedings{ms:ppdp03, Author = {Marino Miculan and Ivan Scagnetto}, Booktitle = {Proc. PPDP'03}, Editor = {Dale Miller}, Pages = {184--194}, Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/PPDP03.pdf}, Publisher = {ACM Press}, Title = {A Framework for Typed {HOAS} and Semantics}, Year = 2003}`

- Pietro Di Gianantonio and Marino Miculan. A unifying approach to recursive and co-recursive definitions. In Herman Geuvers and Freek Wiedijk, editors,
*Proc. types’02*, volume 2646 of*Lecture Notes in Computer Science*, pages 148-161. Springer-Verlag, 2003.

[Bibtex]`@inproceedings{dgm:types02, Author = {Di Gianantonio, Pietro and Marino Miculan}, Booktitle = {Proc. TYPES'02}, Editor = {Herman Geuvers and Freek Wiedijk}, Pages = {148--161}, Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/TYPES02.pdf}, Publisher = {Springer-Verlag}, Series = LNCS, Title = {A Unifying Approach to Recursive and Co-recursive Definitions}, Volume = 2646, Year = 2003}`

- Alberto Ciaffaglione, Luigi Liquori, and Marino Miculan. Imperative object-based calculi in (co)inductive type theories. In Moshe Y. Vardi and Andrei Voronkov, editors,
*Proc. lpar*, volume 2850 of*Lecture Notes in Computer Science*, pages 59-77. Springer, 2003.

[Bibtex]`@inproceedings{clm:lpar03, Author = {Alberto Ciaffaglione and Luigi Liquori and Marino Miculan}, Bibsource = {DBLP, http://dblp.uni-trier.de}, Booktitle = {Proc. LPAR}, Editor = {Moshe Y. Vardi and Andrei Voronkov}, Isbn = {3-540-20101-7}, Pages = {59--77}, Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/LPAR03.pdf}, Publisher = {Springer}, Series = LNCS, Title = {Imperative Object-based Calculi in (Co)Inductive Type Theories}, Volume = 2850, Year = 2003}`

- Furio Honsell, Marino Miculan, and Alberto Momigliano, editors.
*Mechanized reasoning about languages with variable binding*, ACM Digital Library. ACM, 2003.

[Bibtex]`@proceedings{merlin03, Author = {Furio Honsell and Marino Miculan and Alberto Momigliano}, Booktitle = {Proc. 2nd MERLIN}, Date-Modified = {2015-01-15 12:24:08 +0000}, Editor = {Furio Honsell and Marino Miculan and Alberto Momigliano}, Organization = {ACM}, Series = {ACM Digital Library}, Title = {Mechanized Reasoning about Languages with Variable Binding}, Url = {http://dl.acm.org/citation.cfm?id=1088454}, Year = 2003, Bdsk-Url-1 = {http://dl.acm.org/citation.cfm?id=1088454}}`

- Alberto Ciaffaglione, Luigi Liquori, and Marino Miculan. Reasoning on an imperative object-based calculus in higher order abstract syntax. In Furio Honsell, Marino Miculan, and Alberto Momigliano, editors,
*Proc. 2nd merlin*, ACM Digital Library. ACM,, 2003.

[Bibtex]`@inproceedings{clm:merlin03, Author = {Alberto Ciaffaglione and Luigi Liquori and Marino Miculan}, Booktitle = {Proc. 2nd MERLIN}, Editor = {Furio Honsell and Marino Miculan and Alberto Momigliano}, Organization = {ACM}, Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/MERLIN03.pdf}, Series = {ACM Digital Library}, Title = {Reasoning on an Imperative Object-based Calculus in Higher Order Abstract Syntax}, Year = 2003}`

### 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]`@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}}`

- Roberto Bruni, Furio Honsell, Marina Lenisa, and Marino Miculan. Comparing higher-order encodings in logical frameworks and tile logic.
*Electronic notes in theoretical computer science*, 62:136-156, 2002.

[Bibtex]`@article{bruni2002comparing, title={Comparing higher-order encodings in logical frameworks and tile logic}, author={Bruni, Roberto and Honsell, Furio and Lenisa, Marina and Miculan, Marino}, journal={Electronic Notes in Theoretical Computer Science}, volume={62}, pages={136--156}, year={2002}, pdf="http://users.dimi.uniud.it/~marino.miculan/Papers/TOSCA02.pdf", publisher={Elsevier} }`

### 2001

- Furio Honsell, Marino Miculan, and Ivan Scagnetto. An axiomatic approach to metareasoning on systems in higher-order abstract syntax. In
*Proc. icalp’01*, volume 2076 of*Lecture Notes in Computer Science*, pages 963-978. Springer-Verlag, 2001.

[Bibtex]`@inproceedings{hms:icalp01, Author = {Furio Honsell and Marino Miculan and Ivan Scagnetto}, Booktitle = {Proc. ICALP'01}, Pages = {963-978}, Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/ICALP01.pdf}, Publisher = {Springer-Verlag}, Series = LNCS, Title = {An axiomatic approach to metareasoning on systems in higher-order abstract syntax}, Volume = 2076, Year = 2001}`

- Marino Miculan. Developing (meta)theory of lambda-calculus in the theory of contexts. In Simon Ambler, Roy Crole, and Alberto Momigliano, editors,
*Proc. merlin 2001*, volume 58.1 of*Electronic Notes in Theoretical Computer Science*, pages 1-22. Elsevier, 2001.

[Bibtex]`@inproceedings{miculan:merlin01, Author = {Marino Miculan}, Booktitle = {Proc. MERLIN 2001}, Editor = {Simon Ambler and Roy Crole and Alberto Momigliano}, Pages = {1-22}, Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/MERLIN01.pdf}, Publisher = {Elsevier}, Series = ENTCS, Title = {Developing (Meta)Theory of Lambda-calculus in the Theory of Contexts}, Volume = {58.1}, Year = 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]`@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]`@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}`

- Furio Honsell and Marino Miculan, editors.
*Proceedings of fossacs 2001*, volume 2030 of*LNCS*Springer-Verlag, 2001.

[Bibtex]`@proceedings{fossacs01, Author = {Furio Honsell and Marino Miculan}, Booktitle = {Proc. FOSSACS}, Date-Modified = {2015-01-15 12:24:50 +0000}, Editor = {Furio Honsell and Marino Miculan}, Publisher = {Springer-Verlag}, Series = {LNCS}, Title = {Proceedings of FOSSACS 2001}, Url = {http://www.springer.com/computer/theoretical+computer+science/book/978-3-540-41864-1}, Volume = 2030, Year = 2001, Bdsk-Url-1 = {http://www.springer.com/computer/theoretical+computer+science/book/978-3-540-41864-1}}`

- Marina Lenisa and Marino Miculan, editors.
*Proceedings of tosca 2001 – theory of concurrency, higher order languages and types*, volume 62 of*ENTCS*Elsevier, 2001.

[Bibtex]`@proceedings{tosca01, Author = {Marina Lenisa and Marino Miculan}, Booktitle = {Proc. TOSCA'01}, Date-Modified = {2015-01-15 12:24:38 +0000}, Editor = {Marina Lenisa and Marino Miculan}, Publisher = {Elsevier}, Series = {ENTCS}, Title = {Proceedings of TOSCA 2001 - Theory of Concurrency, Higher Order Languages and Types}, Url = {http://www.sciencedirect.com/science/journal/15710661/62}, Volume = 62, Year = 2001, Bdsk-Url-1 = {http://www.sciencedirect.com/science/journal/15710661/62}}`

- Furio Honsell, Marino Miculan, and Ivan Scagnetto. The theory of contexts for first-order and higher-order abstract syntax. In
*Proc. tosca’01*, volume 62 of*ENTCS*, pages 111-130. Elsevier, 2001.

[Bibtex]`@inproceedings{hms:lamtoc, Author = {Furio Honsell and Marino Miculan and Ivan Scagnetto}, Booktitle = {Proc. TOSCA'01}, Pages = {111-130}, Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/TOSCA01a.pdf}, Publisher = {Elsevier}, Series = {ENTCS}, Title = {The Theory of Contexts for First-Order and Higher-Order Abstract Syntax}, Volume = 62, Year = 2001}`

### 1999

- Marino Miculan. Formalizing a lazy substitution proof system for µ-calculus in the calculus of inductive constructions. In
*Proc. icalp’99*, volume 1644 of*Lecture Notes in Computer Science*, Praha, 1999. EATCS, Springer-Verlag.

[Bibtex]`@inproceedings{miculan:icalp99, Address = {Praha}, Author = {Marino Miculan}, Booktitle = {Proc. ICALP'99}, Organization = {EATCS}, Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/ICALP99.pdf}, Publisher = {Springer-Verlag}, Series = LNCS, Title = {Formalizing a lazy substitution proof system for µ-calculus in the Calculus of Inductive Constructions}, Volume = 1644, Year = 1999}`

### 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]`@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]`@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}`

### 1997

- Marino Miculan.
*Encoding logical theories of programs*. PhD thesis, Dipartimento di Informatica, Università di Pisa, Italy, 1997.

[Bibtex]`@phdthesis{mik:eltop, Address = {Italy}, Author = {Marino Miculan}, Number = {TD-7/97}, Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/thesis.pdf}, School = {Dipartimento di Informatica, Universit{\`a} di Pisa}, Title = {Encoding Logical Theories of Programs}, Year = 1997}`

### 1995

- Furio Honsell and Marino Miculan. A natural deduction approach to dynamic logics. In Stefano Berardi and Mario Coppo, editors,
*Proc. types’95*, volume 1158 of*Lecture Notes in Computer Science*, pages 165-182, Turin, 1995. Springer-Verlag.

[Bibtex]`@inproceedings{hm:ndadl, Address = {Turin}, Author = {Furio Honsell and Marino Miculan}, Booktitle = {Proc. TYPES'95}, Editor = {Stefano Berardi and Mario Coppo}, Pages = {165-182}, Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/TYPES95.pdf}, Publisher = {Springer-Verlag}, Series = LNCS, Title = {A Natural Deduction Approach to Dynamic Logics}, Volume = 1158, Year = 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]`@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}`

### 1994

- Marino Miculan. The expressive power of structural operational semantics with explicit assumptions. In Henk Barendregt and Tobias Nipkow, editors,
*Types for proofs and programs, international workshop types’93, nijmegen, the netherlands, may 24-28, 1993, selected papers*, volume 806 of*Lecture Notes in Computer Science*, pages 263-290. Springer, 1994.

[Bibtex]`@inproceedings{mik:enos, author = {Marino Miculan}, editor = {Henk Barendregt and Tobias Nipkow}, title = {The Expressive Power of Structural Operational Semantics with Explicit Assumptions}, booktitle = {Types for Proofs and Programs, International Workshop TYPES'93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers}, series = {Lecture Notes in Computer Science}, volume = {806}, pages = {263--290}, publisher = {Springer}, year = {1994}, url = {http://dx.doi.org/10.1007/3-540-58085-9_80}, Pdf = {http://users.dimi.uniud.it/~marino.miculan/Papers/TYPES93.pdf}, doi = {10.1007/3-540-58085-9_80}, timestamp = {Tue, 14 Jun 2011 20:35:58 +0200}, biburl = {http://dblp.uni-trier.de/rec/bib/conf/types/Miculan93}, bibsource = {dblp computer science bibliography, http://dblp.org} }`