2024
- Vincenzo Riccio, Giancarlo Sorrentino, Ettore Zamponi, Matteo Camilli, Raffaela Mirandola, and Patrizia Scandurra. RAMSES: an artifact exemplar for engineering self-adaptive microservice applications. In Seams@icse, page 161–167. ACM, 2024.
[Bibtex]@inproceedings{DBLP:conf/seams/RiccioSZCMS24, author = {Vincenzo Riccio and Giancarlo Sorrentino and Ettore Zamponi and Matteo Camilli and Raffaela Mirandola and Patrizia Scandurra}, title = {{RAMSES:} An Artifact Exemplar for Engineering Self-Adaptive Microservice Applications}, booktitle = {SEAMS@ICSE}, pages = {161--167}, publisher = {{ACM}}, year = {2024} } - Pietro Di Gianantonio and Abbas Edalat. A cartesian closed category for random variables. In LICS, pages 32:1–32:14. ACM, 2024.
[Bibtex]@inproceedings{DBLP:conf/lics/GianantonioE24, author = {Pietro Di Gianantonio and Abbas Edalat}, title = {A Cartesian Closed Category for Random Variables}, booktitle = {{LICS}}, pages = {32:1--32:14}, publisher = {{ACM}}, year = {2024} } - Angelo Odetti, Gabriele Bruzzone, Roberta Ferretti, Simona Aracri, Federico Carotenuto, Carolina Vagnoli, Alessandro Zaldei, and Ivan Scagnetto. Lake environmental data harvester (LED) for alpine lake monitoring with autonomous surface vehicles (asvs). Remote. sens., 16(11):1998, 2024.
[Bibtex]@article{DBLP:journals/remotesensing/OdettiBFACVZS24, author = {Angelo Odetti and Gabriele Bruzzone and Roberta Ferretti and Simona Aracri and Federico Carotenuto and Carolina Vagnoli and Alessandro Zaldei and Ivan Scagnetto}, title = {Lake Environmental Data Harvester {(LED)} for Alpine Lake Monitoring with Autonomous Surface Vehicles (ASVs)}, journal = {Remote. Sens.}, volume = {16}, number = {11}, pages = {1998}, year = {2024} } - Matteo Paier, Mattia Pizzolitto, Gian Luca Foresti, and Marino Miculan. Netstaldi: A modular distributed architecture for incremental network discovery. In Gianni D’Angelo, Flaminia Luccio, and Francesco Palmieri, editors, Proceedings of the 8th italian conference on cyber security (ITASEC 2024), volume 3731 of {CEUR} Workshop Proceedings. Ceur-ws.org, 2024.
[Bibtex]![[PDF]](https://mads.uniud.it/wp-content/plugins/papercite/img/pdf.png)
![[url]](https://mads.uniud.it/wp-content/papercite-data/img/folder.png)
@inproceedings{ppfm:itasec24, author = {Matteo Paier and Mattia Pizzolitto and Foresti, Gian Luca and Marino Miculan}, editor = {Gianni D'Angelo and Flaminia Luccio and Francesco Palmieri}, title = {Netstaldi: {A} Modular Distributed Architecture for Incremental Network Discovery}, booktitle = {Proceedings of the 8th Italian Conference on Cyber Security ({ITASEC} 2024)}, location = {Salerno, Italy, April 8-12, 2024}, series = {{CEUR} Workshop Proceedings}, volume = 3731, publisher = {CEUR-WS.org}, year = 2024, pdf = {https://ceur-ws.org/Vol-3731/paper37.pdf}, url = {https://ceur-ws.org/Vol-3731} } - Roberto Van Eeden, Matteo Paier, and Marino Miculan. A formal analysis of CIE level 2 multi-factor authentication via SMS OTP. In Proceedings of the 21st international conference on security and cryptography – secrypt, pages 483-491. INSTICC, Scitepress, 2024.
[Bibtex]![[DOI]](https://mads.uniud.it/wp-content/plugins/papercite/img/external.png)
@inproceedings{vepm:secrypt24, author={Van Eeden, Roberto and Matteo Paier and Marino Miculan}, title={A Formal Analysis of {CIE} Level 2 Multi-Factor Authentication via {SMS OTP}}, booktitle={Proceedings of the 21st International Conference on Security and Cryptography - SECRYPT}, year={2024}, pages={483-491}, publisher={SciTePress}, organization={INSTICC}, doi={10.5220/0012768300003767}, url = {https://doi.org/10.5220/0012768300003767}, isbn={978-989-758-709-2}, issn={2184-7711}, selected = true, abstract = {We analyze the security of Level 2 multi-factor authentication (MFA) based on SMS One-Time Passcode (OTP) of Italian Electronic Identity Card (CIE). We propose a novel threat model encompassing password compromise, network disruptions, user errors, and malware attacks. The combinations of the adversary’s attack capabilites yield a plethora of possible attack scenarios, which we systematically generate, formalise and verify in ProVerif. Our analysis reveals that CIE MFA based on SMS OTP is vulnerable to attacks with read access to the mobile device or keyboard, or to phishing, but event to mere read access to the user’s computer screen. To address the latter vulnerability, we propose a minor modification of the protocol. The threat model we introduce paves the way for the analysis of other CIE MFA protocols.} } - Michele Pasqua and Marino Miculan. Behavioral equivalences for AbU: verifying security and safety in distributed iot systems. Theoretical computer science, 998:114537, 2024.
[Bibtex]
@article{PASQUA2024114537, title = {Behavioral equivalences for {AbU}: Verifying security and safety in distributed IoT systems}, journal = {Theoretical Computer Science}, volume = {998}, pages = {114537}, year = {2024}, issn = {0304-3975}, doi = {10.1016/j.tcs.2024.114537}, url = {https://www.sciencedirect.com/science/article/pii/S030439752400152X}, author = {Michele Pasqua and Marino Miculan}, keywords = {ECA rules, IoT programming, Distributed systems, Bisimulations, Formal methods, Autonomic computing, Verification}, abstract = {Attribute-based memory Updates (Image 1in short) is an interaction mechanism recently introduced for adapting the Event-Condition-Action (ECA) programming paradigm to distributed reactive systems, such as autonomic and smart IoT device ensembles. In this model, an event (e.g., an input from a sensor, or a device state update) can trigger an ECA rule, whose execution can cause the state update of (possibly) many remote devices at once; the latter are selected “on the fly” by means of predicates over their state, without the need of a central coordinating entity. However, the combination of different Image 1systems may yield unexpected interactions, e.g., when a new device is added to an existing secure system, potentially hindering the security of the whole ensemble of devices. This can be critical in the IoT, where smart devices are more and more pervasive in our daily life. In this paper, we consider the problem of ensuring security and safety requirements for Image 1systems (and, in turn, for IoT devices). The first are a form of noninterference, as they correspond to avoid forbidden information flows (e.g., information flows violating confidentiality); while the second are a form of non-interaction, as they correspond to avoid unintended executions (e.g., leading to erroneous/unsafe states). In order to formally model these requirements, we introduce suitable behavioral equivalences for Image 1. These equivalences are generalizations of hiding bisimilarity, i.e., a kind of weak bisimilarity where we can compare systems up to actions at different levels of security. Leveraging these behavioral equivalences, we propose (syntactic) sufficient conditions guaranteeing the requirements and, then, effective algorithms for statically verifying such conditions.}, selected=true } - Davide Castelnovo, Fabio Gadducci, and Marino Miculan. A simple criterion for 𝓜,𝓝-adhesivity. Theoretical computer science, 982:114280, 2024.
[Bibtex]
@article{CASTELNOVO2024114280, title = {A simple criterion for 𝓜,𝓝-adhesivity}, journal = {Theoretical Computer Science}, volume = {982}, pages = {114280}, year = {2024}, issn = {0304-3975}, doi = {10.1016/j.tcs.2023.114280}, url = {https://www.sciencedirect.com/science/article/pii/S0304397523005935}, author = {Davide Castelnovo and Fabio Gadducci and Marino Miculan}, abstract = {Adhesive categories, and variants such as 𝓜,𝓝-adhesive ones, marked a watershed moment for the algebraic approaches to the rewriting of graph-like structures, since they provide an abstract framework where many general results (on e.g. parallelism) could be recast and uniformly proved. However, often checking that a model satisfies the adhesivity properties is far from immediate. In this paper we present a new criterion giving a sufficient condition for 𝓜,𝓝-adhesivity, a generalisation of the original notion of adhesivity. To show the effectiveness of this criterion, we apply it to several existing categories of graph-like structures, including hypergraphs, various kinds of hierarchical graphs (a formalism that is notoriously difficult to fit in the mould of algebraic approaches to rewriting), and combinations of them.}, selected=false }
2023
- Vincenzo Riccio, Giancarlo Sorrentino, Matteo Camilli, Raffaela Mirandola, and Patrizia Scandurra. Engineering self-adaptive microservice applications: an experience report. In ICSOC (1), volume 14419 of Lecture Notes in Computer Science, page 227–242. Springer, 2023.
[Bibtex]@inproceedings{DBLP:conf/icsoc/RiccioSCMS23, author = {Vincenzo Riccio and Giancarlo Sorrentino and Matteo Camilli and Raffaela Mirandola and Patrizia Scandurra}, title = {Engineering Self-adaptive Microservice Applications: An Experience Report}, booktitle = {{ICSOC} {(1)}}, series = {Lecture Notes in Computer Science}, volume = {14419}, pages = {227--242}, publisher = {Springer}, year = {2023} } - Cybersecurity Lab. Cve-2023-40718: ips engine evasion using custom tcp flags. 2023.
[Bibtex]
@misc{mm:cve2023, author={Cybersecurity Lab}, title={CVE-2023-40718: IPS Engine evasion using custom TCP flags}, url ={https://www.fortiguard.com/psirt/FG-IR-23-090}, year=2023, publisher={Fortinet} } - Marino Miculan and Matteo Paier. Assembling coherent network topologies using round-trip graphs. In Proceedings of the 24th italian conference on theoretical computer science, ictcs 2023, volume 3587 of {CEUR} Workshop Proceedings, page 110–115. Ceur-ws.org, 2023.
[Bibtex]
@inproceedings{DBLP:conf/ictcs/MiculanP23, author = {Marino Miculan and Matteo Paier}, title = {Assembling Coherent Network Topologies Using Round-Trip Graphs}, booktitle = {Proceedings of the 24th Italian Conference on Theoretical Computer Science, ICTCS 2023}, series = {{CEUR} Workshop Proceedings}, volume = 3587, pages = {110--115}, publisher = {CEUR-WS.org}, year = 2023, pdf = {https://ceur-ws.org/Vol-3587/6692.pdf}, url = {https://ceur-ws.org/Vol-3587/} } - Gian Luca Foresti, Axel De Nardin, Alessio Fiorin, Marino Miculan, and Claudio Piciarelli. Exploiting maximum likelihood to improve network traffic deanonymization performances. Strategic leadership journal, 1:101-113, 2023.
[Bibtex]
@article{slj23, author={Foresti, Gian Luca and De Nardin, Axel and Fiorin, Alessio and Miculan, Marino and Claudio Piciarelli}, journal={Strategic Leadership Journal}, title={Exploiting maximum likelihood to improve network traffic deanonymization performances}, year=2023, volume=1, pages={101-113}, issn={2975-0148}, isbn={9791255150497}, PDF={https://www.difesa.it/SMD_/CASD/IM/CeMiSS/DocumentiVis/Rivista_Scientifica/Rivista_scientifica_n_1.pdf}, selected=false } - Gabriele Voltan, Gian Luca Foresti, and Marino Miculan. Pairing an autoencoder and a SF-SOINN for implementing an intrusion detection system. In Proceedings of the thematic workshops co-located with the 3rd CINI national lab AIIS conference on artificial intelligence (ital-IA 2023), volume 3486 of {CEUR} Workshop Proceedings, page 409–414. Ceur-ws.org, 2023.
[Bibtex]
@inproceedings{DBLP:conf/ital-ia/VoltanFM23, author = {Gabriele Voltan and Foresti, Gian Luca and Marino Miculan}, title = {Pairing an Autoencoder and a {SF-SOINN} for Implementing an Intrusion Detection System}, booktitle = {Proceedings of the Thematic Workshops co-located with the 3rd {CINI} National Lab {AIIS} Conference on Artificial Intelligence (Ital-{IA} 2023)}, series = {{CEUR} Workshop Proceedings}, volume = {3486}, pages = {409--414}, publisher = {CEUR-WS.org}, year = {2023}, pdf = {https://ceur-ws.org/Vol-3486/23.pdf}, url = {https://ceur-ws.org/Vol-3486} } - Stefano Bistarelli, Francesco Faloci, Paolo Mori, Carlo Taticchi, and Marino Miculan. Modeling Carne PRI supply chain with the *-chain platform. In Paolo Mori, Ivan Visconti, and Stefano Bistarelli, editors, Proceedings of the fifth distributed ledger technology workshop (DLT 2023), bologna, italy, may 25-26, 2023, volume 3460 of {CEUR} Workshop Proceedings. Ceur-ws.org, 2023.
[Bibtex]
@inproceedings{DBLP:conf/dlt2/BistarelliFMTM23, author = {Stefano Bistarelli and Francesco Faloci and Paolo Mori and Carlo Taticchi and Marino Miculan}, editor = {Paolo Mori and Ivan Visconti and Stefano Bistarelli}, title = {Modeling {Carne PRI} supply chain with the *-Chain Platform}, booktitle = {Proceedings of the Fifth Distributed Ledger Technology Workshop {(DLT} 2023), Bologna, Italy, May 25-26, 2023}, series = {{CEUR} Workshop Proceedings}, volume = {3460}, publisher = {CEUR-WS.org}, year = {2023}, url ={https://ceur-ws.org/Vol-3460/}, pdf = {https://ceur-ws.org/Vol-3460/papers/DLT\_2023\_paper\_10.pdf} } - Andrea Altarui, Marino Miculan, and Matteo Paier. DBCChecker: a bigraph-based tool for checking security properties of container compositions. In Francesco Buccafurri, Elena Ferrari, and Gianluca Lax, editors, Proceedings of the italian conference on cyber security (ITASEC 2023), bari, italy, may 2-5, 2023, volume 3488 of {CEUR} Workshop Proceedings. Ceur-ws.org, 2023.
[Bibtex]
@inproceedings{DBLP:conf/itasec/AltaruiMP23, author = {Andrea Altarui and Marino Miculan and Matteo Paier}, editor = {Francesco Buccafurri and Elena Ferrari and Gianluca Lax}, title = {{DBCChecker}: a Bigraph-based Tool for Checking Security Properties of Container Compositions}, booktitle = {Proceedings of the Italian Conference on Cyber Security ({ITASEC} 2023), Bari, Italy, May 2-5, 2023}, series = {{CEUR} Workshop Proceedings}, volume = {3488}, publisher = {CEUR-WS.org}, year = {2023}, pdf = {https://ceur-ws.org/Vol-3488/paper01.pdf}, html = {https://ceur-ws.org/Vol-3488} } - Michele Pasqua and Marino Miculan. AbU: a calculus for distributed event-driven programming with attribute-based interaction. Theoretical computer science, 958:113841, 2023.
[Bibtex]
@article{PASQUA2023113841, title = {{AbU}: A calculus for distributed event-driven programming with attribute-based interaction}, journal = {Theoretical Computer Science}, volume = 958, pages = {113841}, year = 2023, issn = {0304-3975}, doi = {https://doi.org/10.1016/j.tcs.2023.113841}, url = {https://www.sciencedirect.com/science/article/pii/S0304397523001548}, author = {Michele Pasqua and Marino Miculan}, selected = true, keywords = {ECA rules, Attribute-based communication, Distributed systems, Formal methods, Edge computing, IoT programming}, abstract = {In recent years, event-driven programming languages, in particular those based on Event Condition Action (ECA) rules, have emerged as a promising paradigm for implementing ubiquitous and pervasive systems. These implementations are mostly centralized, where a single server (often in the cloud) collects and processes all the inputs from the environment. In fact, placing the computation on the nodes interacting with the environment requires suitable abstractions for effective communication and coordination of (possibly large) ensembles of these distributed components — abstractions that current ECA languages are still missing. To this end, in this paper we present AbU, a calculus for modeling and reasoning about ECA-based systems with attribute-based communication. The latter is an interaction model recently introduced for the coordination of (possibly large) families of nodes: communication is similar to broadcast but the actual receivers are selected on the spot, by means of predicates over nodes properties. Thus, the programmer can specify interactions between nodes in a declarative way, abstracting from details such as nodes identity, number, or even their existence, without the need for a central server: the computation is moved on the “edge”, thus improving reliability, scalability, privacy and security. After having defined syntax and formal semantics of AbU, we showcase its expressiveness by providing some example applications and the encoding of AbC, the archetypal calculus with attribute-based communication. Then, we focus on two key properties of reactive systems: stabilization (i.e., termination of internal steps) and confluence. For both these properties we provide formal semantic definition, sufficient syntactic conditions on AbU systems, and algorithms to statically check such conditions. Hence, AbU is both a basis for the formal analysis of event-driven architectures with attributed-based interaction, and a reference model for a full-fledged language for IoT and edge computing.} } - Marino Miculan and Nicola Vitacolonna. Automated verification of telegram’s mtproto 2.0 in the symbolic model. Computers & security, page 103072, 2023.
[Bibtex]
@article{MICULAN2022103072, title = {Automated Verification of Telegram’s MTProto 2.0 in the Symbolic Model}, journal = {Computers & Security}, pages = {103072}, year = {2023}, issn = {0167-4048}, doi = {10.1016/j.cose.2022.103072}, url = {https://doi.org/10.1016/j.cose.2022.103072}, author = {Marino Miculan and Nicola Vitacolonna}, keywords = {Specification, Verification and Synthesis, Security protocols, Practical verification, Privacy, Formal methods}, abstract = {MTProto 2.0 is the suite of security protocols for instant messaging at the core of the popular Telegram messenger application. In this paper we analyse MTProto 2.0 using ProVerif, a state-of-the-art symbolic security protocol verifier based on the Dolev-Yao model. We provide the first formal symbolic model of MTProto 2.0; in this model, we provide fully automated proofs of the soundness of authentication, normal chat, end-to-end encrypted chat, and rekeying mechanisms with respect to several security properties, including authentication, integrity, secrecy and perfect forward secrecy. At the same time, we discover that the rekeying protocol is vulnerable to an unknown key-share (UKS) attack. To achieve these results, we proceed in an incremental way: each protocol is examined in isolation, relying only on the guarantees provided by the previous ones and the robustness of the basic cryptographic primitives. The importance of this research is threefold. First, it proves the formal correctness of MTProto 2.0 with respect to most relevant security properties. Secondly, we isolate the aspects of cryptographic primitives that escape the symbolic model and thus require further investigation in the computational model. Finally, our modelisation can serve as a reference for the implementation and analysis of clients and servers.}, selected=true } - Claude Stolze, Marino Miculan, and Pietro Di Gianantonio. Composable partial multiparty session types for open systems. Software and systems modeling, (22):473-494, 2023.
[Bibtex]
@article{stolze2022composable, title={Composable partial multiparty session types for open systems}, author={Stolze, Claude and Miculan, Marino and Di Gianantonio, Pietro}, journal={Software and Systems Modeling}, year=2023, url = {https://doi.org/10.1007/s10270-022-01040-x}, doi = {10.1007/s10270-022-01040-x}, publisher={Springer}, pages = {473-494}, number=22, keywords={concurrency,session types,process calculi,compositionality}, selected=true }
2022
- Pietro Di Gianantonio, Abbas Edalat, and Ran Gutin. A language for evaluating derivatives of functionals using automatic differentiation. In MFPS, volume 3 of {EPTICS}. Episciences, 2022.
[Bibtex]@inproceedings{DBLP:journals/corr/abs-2210-06095, author = {Pietro Di Gianantonio and Abbas Edalat and Ran Gutin}, title = {A language for evaluating derivatives of functionals using automatic differentiation}, booktitle = {{MFPS}}, series = {{EPTICS}}, volume = {3}, publisher = {EpiSciences}, year = {2022} } - Michele Pasqua, Massimo Comuzzo, and Marino Miculan. The abu language: iot distributed programming made easy. Ieee access, 10:132763-132776, 2022.
[Bibtex]
@article{pcm:access22, author={Pasqua, Michele and Comuzzo, Massimo and Miculan, Marino}, journal={IEEE Access}, title={The AbU Language: IoT Distributed Programming Made Easy}, year=2022, volume=10, pages={132763-132776}, doi={10.1109/ACCESS.2022.3230287}, url ={https://doi.org/10.1109/ACCESS.2022.3230287}, selected=false } - Lorenzo Bazzana, Marino Miculan, and Michele Codutti. Cve-2022-3203: oring net iap-420(+) hidden functionality. 2022.
[Bibtex]
@misc{bmc:cve2022, author={Lorenzo Bazzana and Marino Miculan and Michele Codutti}, title={CVE-2022-3203: ORing net IAP-420(+) Hidden Functionality}, url ={https://www.cve.org/CVERecord?id=CVE-2022-3203}, year=2022, publisher={MITRE} } - Alessio Chiapperini, Marino Miculan, and Marco Peressotti. Computing (optimal) embeddings of directed bigraphs. Sci. comput. program., 221:102842, 2022.
[Bibtex]
@article{DBLP:journals/scp/ChiapperiniMP22, author = {Alessio Chiapperini and Marino Miculan and Marco Peressotti}, title = {Computing (optimal) embeddings of directed bigraphs}, journal = {Sci. Comput. Program.}, volume = {221}, pages = {102842}, year = {2022}, url = {https://doi.org/10.1016/j.scico.2022.102842}, doi = {10.1016/j.scico.2022.102842}, selected=false } - Marino Miculan and Matteo Paier. A calculus for subjective communication. In Ugo Dal Lago and Daniele Gorla, editors, Proceedings of the 23rd italian conference on theoretical computer science, ICTCS 2022, rome, italy, september 7-9, 2022, volume 3284 of {CEUR} Workshop Proceedings, page 148–160. Ceur-ws.org, 2022.
[Bibtex]
@inproceedings{DBLP:conf/ictcs/MiculanP22, author = {Marino Miculan and Matteo Paier}, editor = {Dal Lago, Ugo and Daniele Gorla}, title = {A Calculus for Subjective Communication}, booktitle = {Proceedings of the 23rd Italian Conference on Theoretical Computer Science, {ICTCS} 2022, Rome, Italy, September 7-9, 2022}, series = {{CEUR} Workshop Proceedings}, volume = {3284}, pages = {148--160}, publisher = {CEUR-WS.org}, year = {2022}, pdf = {http://ceur-ws.org/Vol-3284/1841.pdf} } - Michele Pasqua and Marino Miculan. Distributed programming of smart systems with event-condition-action rules. In Ugo Dal Lago and Daniele Gorla, editors, Proceedings of the 23rd italian conference on theoretical computer science, ICTCS 2022, rome, italy, september 7-9, 2022, volume 3284 of {CEUR} Workshop Proceedings, page 201–206. Ceur-ws.org, 2022.
[Bibtex]
@inproceedings{DBLP:conf/ictcs/PasquaM22, author = {Michele Pasqua and Marino Miculan}, editor = {Dal Lago, Ugo and Daniele Gorla}, title = {Distributed Programming of Smart Systems with Event-Condition-Action Rules}, booktitle = {Proceedings of the 23rd Italian Conference on Theoretical Computer Science, {ICTCS} 2022, Rome, Italy, September 7-9, 2022}, series = {{CEUR} Workshop Proceedings}, volume = {3284}, pages = {201--206}, publisher = {CEUR-WS.org}, year = {2022}, pdf = {http://ceur-ws.org/Vol-3284/7982.pdf} } - Davide Castelnovo, Fabio Gadducci, and Marino Miculan. A new criterion for m,n-adhesivity, with an application to hierarchical graphs. In Proc.~fossacs, volume 13242 of Lecture Notes in Computer Science, page 205–224. Springer, 2022.
[Bibtex]
@inproceedings{DBLP:conf/fossacs/CastelnovoGM22, author = {Davide Castelnovo and Fabio Gadducci and Marino Miculan}, title = {A new criterion for M,N-adhesivity, with an application to hierarchical graphs}, booktitle = {Proc.~FoSSaCS}, series = {Lecture Notes in Computer Science}, volume = {13242}, pages = {205--224}, publisher = {Springer}, url = {https://doi.org/10.1007/978-3-030-99253-8\_11}, doi = {10.1007/978-3-030-99253-8\_11}, year = {2022} } - A. Chiapperini, M. Miculan, and M. Peressotti. Computing (optimal) embeddings of directed bigraphs. Science of computer programming, 221, 2022.
[Bibtex]
@ARTICLE{Chiapperini2022, author={Chiapperini, A. and Miculan, M. and Peressotti, M.}, title={Computing (optimal) embeddings of directed bigraphs}, journal={Science of Computer Programming}, year={2022}, volume={221}, doi={10.1016/j.scico.2022.102842}, art_number={102842}, url={https://www.scopus.com/inward/record.uri?eid=2-s2.0-85135478850&doi=10.1016%2fj.scico.2022.102842&partnerID=40&md5=3f11cc6664deac513829b50e0524e732}, } - D. Castelnovo and M. Miculan. Fuzzy algebraic theories. In Proc. csl 2022, volume 216, 2022.
[Bibtex]
@inproceedings{Castelnovo2022, author={Castelnovo, D. and Miculan, M.}, title={Fuzzy Algebraic Theories}, booktitle={Proc. CSL 2022}, journal={Leibniz International Proceedings in Informatics, LIPIcs}, year={2022}, volume={216}, doi={10.4230/LIPIcs.CSL.2022.13}, art_number={13}, url={https://www.scopus.com/inward/record.uri?eid=2-s2.0-85124183018&doi=10.4230%2fLIPIcs.CSL.2022.13&partnerID=40&md5=709f772eda711fb0fc73da9600ce19fc}, } - C. Stolze, M. Miculan, and P. Di Gianantonio. Composable partial multiparty session types for open systems. Software and systems modeling, 2022.
[Bibtex]
@ARTICLE{Stolze2022, author={Stolze, C. and Miculan, M. and Di Gianantonio, P.}, title={Composable partial multiparty session types for open systems}, journal={Software and Systems Modeling}, year={2022}, doi={10.1007/s10270-022-01040-x}, url={https://www.scopus.com/inward/record.uri?eid=2-s2.0-85138851121&doi=10.1007%2fs10270-022-01040-x&partnerID=40&md5=3e8f09832fa068961ea01901276ccff1}, } - D. Castelnovo, F. Gadducci, and M. Miculan. A new criterion for m,n-adhesivity, with an application to hierarchical graphs. Lecture notes in computer science, 13242 LNCS:205-224, 2022.
[Bibtex]
@ARTICLE{Castelnovo2022205, author={Castelnovo, D. and Gadducci, F. and Miculan, M.}, title={A new criterion for M,N-adhesivity, with an application to hierarchical graphs}, booktitle={Proc. FOSSACS 2022}, journal={Lecture Notes in Computer Science}, year={2022}, volume={13242 LNCS}, pages={205-224}, doi={10.1007/978-3-030-99253-8_11}, url={https://www.scopus.com/inward/record.uri?eid=2-s2.0-85128472308&doi=10.1007%2f978-3-030-99253-8_11&partnerID=40&md5=091a5ac308a80ee87336375d8ef0a113}, }
2021
- D. Castelnovo and M. Miculan. Closure hyperdoctrines. In Proc. CSL 2021, volume 211, 2021.
[Bibtex]
@CONFERENCE{Castelnovo2021, author={Castelnovo, D. and Miculan, M.}, title={Closure hyperdoctrines}, booktitle={Proc. {CSL} 2021}, journal={Leibniz International Proceedings in Informatics, LIPIcs}, year=2021, volume=211, doi={10.4230/LIPIcs.CALCO.2021.12}, url={https://www.scopus.com/inward/record.uri?eid=2-s2.0-85120635973&doi=10.4230%2fLIPIcs.CALCO.2021.12&partnerID=40&md5=ce7faf91f3fe625ba20c3403398899a3}, } - M. Pasqua and M. Miculan. On the security and safety of AbU systems. Lecture notes in computer science, 13085:178-198, 2021.
[Bibtex]
@ARTICLE{Pasqua2021178, author={Pasqua, M. and Miculan, M.}, title={On the Security and Safety of {AbU} Systems}, journal={Lecture Notes in Computer Science}, year={2021}, volume=13085, pages={178-198}, doi={10.1007/978-3-030-92124-8_11}, url={https://www.scopus.com/inward/record.uri?eid=2-s2.0-85121933293&doi=10.1007%2f978-3-030-92124-8_11&partnerID=40&md5=2f8730a07845071c20256f5ad54c556c}, } - C. Stolze, M. Miculan, and P. Di Gianantonio. Composable partial multiparty session types. Lecture notes in computer science, 13077:44-62, 2021.
[Bibtex]
@ARTICLE{Stolze202144, author={Stolze, C. and Miculan, M. and Di Gianantonio, P.}, title={Composable Partial Multiparty Session Types}, journal={Lecture Notes in Computer Science}, year={2021}, volume={13077}, pages={44-62}, doi={10.1007/978-3-030-90636-8_3}, url={https://www.scopus.com/inward/record.uri?eid=2-s2.0-85119850638&doi=10.1007%2f978-3-030-90636-8_3&partnerID=40&md5=0437eadf94addb4ef79cc72315fca90c}, } - M. Miculan and M. Pasqua. A calculus for attribute-based memory updates. Lecture notes in computer science (including subseries lecture notes in artificial intelligence and lecture notes in bioinformatics), 12819 LNCS:366-385, 2021.
[Bibtex]
@ARTICLE{Miculan2021366, author={Miculan, M. and Pasqua, M.}, title={A Calculus for Attribute-Based Memory Updates}, journal={Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}, year={2021}, volume={12819 LNCS}, pages={366-385}, doi={10.1007/978-3-030-85315-0_21}, url={https://www.scopus.com/inward/record.uri?eid=2-s2.0-85115166863&doi=10.1007%2f978-3-030-85315-0_21&partnerID=40&md5=f3b6e4a891b628d1891ab70fdf63a4c7}, } - A. de Nardin, M. Miculan, C. Piciarelli, and G. L. Foresti. A time-series classification approach to shallow web traffic de-anonymization. , volume 2940, pages 156-165, 2021.
[Bibtex]
@CONFERENCE{deNardin2021156, author={de Nardin, A. and Miculan, M. and Piciarelli, C. and Foresti, G.L.}, title={A time-series classification approach to shallow web traffic de-anonymization}, journal={CEUR Workshop Proceedings}, year={2021}, volume={2940}, pages={156-165}, url={https://www.scopus.com/inward/record.uri?eid=2-s2.0-85114911106&partnerID=40&md5=8d7ede8cf290c91e4307a05ed703e39c}, } - M. Miculan and N. Vitacolonna. Automated symbolic verification of telegramís mtproto 2.0. , pages 185-197, 2021.
[Bibtex]
@CONFERENCE{Miculan2021185, author={Miculan, M. and Vitacolonna, N.}, title={Automated symbolic verification of Telegramís MTProto 2.0}, journal={Proceedings of the 18th International Conference on Security and Cryptography, SECRYPT 2021}, year={2021}, pages={185-197}, doi={10.5220/0010549601850197}, url={https://www.scopus.com/inward/record.uri?eid=2-s2.0-85111859162&doi=10.5220%2f0010549601850197&partnerID=40&md5=f772a7b44162ef008324c0672276b782}, }
2020
- M. Miculan and M. Peressotti. Software transactional memory with interactions. , volume 2756, 2020.
[Bibtex]
@CONFERENCE{Miculan2020, author={Miculan, M. and Peressotti, M.}, title={Software transactional memory with interactions}, journal={CEUR Workshop Proceedings}, year={2020}, volume={2756}, url={https://www.scopus.com/inward/record.uri?eid=2-s2.0-85098682549&partnerID=40&md5=e1672bc6cca0fbd53487706af205407d}, } - Alessio Chiapperini, Marino Miculan, and Marco Peressotti. Computing embeddings of directed bigraphs. In Fabio Gadducci and Timo Kehrer, editors, Graph transformation – 13th international conference, ICGT 2020, proceedings, volume 12150 of Lecture Notes in Computer Science, page 38–56. Springer, 2020.
[Bibtex]
@inproceedings{cmp:icgt20, author = {Alessio Chiapperini and Marino Miculan and Marco Peressotti}, editor = {Fabio Gadducci and Timo Kehrer}, title = {Computing Embeddings of Directed Bigraphs}, booktitle = {Graph Transformation - 13th International Conference, {ICGT} 2020, Proceedings}, series = {Lecture Notes in Computer Science}, volume = 12150, pages = {38--56}, publisher = {Springer}, year = 2020, url = {https://doi.org/10.1007/978-3-030-51372-6\_3}, doi = {10.1007/978-3-030-51372-6\_3} } - Fabio Burco, Marino Miculan, and Marco Peressotti. Towards a formal model for composable container systems. In Chih -, Tomás Cerný, Dongwan Shin, and Alessio Bechini, editors, SAC’20: the 35th ACM/SIGAPP symposium on applied computing. ACM, 2020.
[Bibtex]
@inproceedings{DBLP:conf/sac/BurcoMP20, author = {Fabio Burco and Marino Miculan and Marco Peressotti}, editor = {Chih{-}Cheng Hung and Tom{\'{a}}s Cern{\'{y}} and Dongwan Shin and Alessio Bechini}, title = {Towards a formal model for composable container systems}, booktitle = {{SAC}'20: The 35th {ACM/SIGAPP} Symposium on Applied Computing}, publisher = {{ACM}}, year = {2020}, url = {https://doi.org/10.1145/3341105.3374121}, doi = {10.1145/3341105.3374121}, timestamp = {Thu, 02 Apr 2020 17:08:04 +0200}, biburl = {https://dblp.org/rec/conf/sac/BurcoMP20.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} } - Marino Miculan and Daniel Tosone. Securing the art market with distributed public ledgers. In Proc. 3rd workshop on distributed ledger technologies (dlt@itasec 2020), volume 2580 of {CEUR} Workshop Proceedings, 2020.
[Bibtex]
@inproceedings{miculantosone20, author = {Marino Miculan and Daniel Tosone}, title = {Securing the Art Market with Distributed Public Ledgers}, booktitle = {Proc. 3rd Workshop on Distributed Ledger Technologies (DLT@ITASEC 2020)}, series = {{CEUR} Workshop Proceedings}, volume = {2580}, url = {http://ceur-ws.org/Vol-2580/DLT\_2020\_paper\_4.pdf}, year = {2020} }
2019
- Luca Geatti, Federico Igne, and Marino Miculan. An abstract distributed middleware for transactions over heterogeneous stores. In Alessandra Cherubini, Nicoletta Sabadini, and Simone Tini, editors, Proc. 20th italian conference on theoretical computer science, ictcs 2019, volume 2504 of {CEUR} Workshop Proceedings, page 171–183. Ceur-ws.org, 2019.
[Bibtex]
@inproceedings{DBLP:conf/ictcs/GeattiIM19, author = {Luca Geatti and Federico Igne and Marino Miculan}, editor = {Alessandra Cherubini and Nicoletta Sabadini and Simone Tini}, title = {An Abstract Distributed Middleware for Transactions over Heterogeneous Stores}, booktitle = {Proc. 20th Italian Conference on Theoretical Computer Science, ICTCS 2019}, series = {{CEUR} Workshop Proceedings}, volume = {2504}, pages = {171--183}, publisher = {CEUR-WS.org}, year = {2019}, pdf = {http://ceur-ws.org/Vol-2504/paper20.pdf}, } - Marco Bernardo and Marino Miculan. Constructive logical characterizations of bisimilarity for reactive probabilistic systems. Theoretical computer science, 764:80–99, 2019.
[Bibtex]
@article{DBLP:journals/tcs/BernardoM19, author = {Marco Bernardo and Marino Miculan}, title = {Constructive logical characterizations of bisimilarity for reactive probabilistic systems}, journal = {Theoretical Computer Science}, volume = 764, pages = {80--99}, year = 2019, url = {https://doi.org/10.1016/j.tcs.2018.12.003}, doi = {10.1016/j.tcs.2018.12.003}, timestamp = {Fri, 12 Apr 2019 09:23:51 +0200}, biburl = {https://dblp.org/rec/bib/journals/tcs/BernardoM19}, bibsource = {dblp computer science bibliography, https://dblp.org} } - Marino Miculan, Gian Luca Foresti, and Claudio Piciarelli. Towards user recognition by shallow web traffic inspection. In Proc. third italian conference on cyber security, volume 2315 of {CEUR} Workshop Proceedings. Ceur, 2019.
[Bibtex]
@inproceedings{DBLP:conf/itasec/MiculanFP19, author = {Marino Miculan and Gian Luca Foresti and Claudio Piciarelli}, title = {Towards User Recognition by Shallow Web Traffic Inspection}, booktitle = {Proc. Third Italian Conference on Cyber Security}, series = {{CEUR} Workshop Proceedings}, volume = 2315, publisher = {CEUR}, year = 2019, url = {http://ceur-ws.org/Vol-2315/paper08.pdf}, timestamp = {Thu, 07 Feb 2019 10:01:27 +0100}, biburl = {https://dblp.org/rec/bib/conf/itasec/MiculanFP19}, bibsource = {dblp computer science bibliography, https://dblp.org} }
2018
- Alessio Mansutti, Marino Miculan, and Marco Peressotti. Loose graph simulations. In Martina Seidl and Steffen Zschaler, editors, Software technologies: applications and foundations – STAF 2017, revised selected papers, volume 10748 of Lecture Notes in Computer Science, page 109–126. Springer, 2018.
[Bibtex]
@inproceedings{DBLP:conf/staf/MansuttiMP17, author = {Alessio Mansutti and Marino Miculan and Marco Peressotti}, editor = {Martina Seidl and Steffen Zschaler}, title = {Loose Graph Simulations}, booktitle = {Software Technologies: Applications and Foundations - {STAF} 2017, Revised Selected Papers}, series = {Lecture Notes in Computer Science}, volume = {10748}, pages = {109--126}, publisher = {Springer}, year = {2018}, url = {https://doi.org/10.1007/978-3-319-74730-9\_9}, doi = {10.1007/978-3-319-74730-9\_9}, timestamp = {Mon, 29 Jan 2018 17:16:10 +0100}, biburl = {https://dblp.org/rec/bib/conf/staf/MansuttiMP17}, bibsource = {dblp computer science bibliography, https://dblp.org} } - Alberto Ciaffaglione, Furio Honsell, Marina Lenisa, and Ivan Scagnetto. The involutions-as-principal types/application-as-unification analogy. In Gilles Barthe, Geoff Sutcliffe, and Margus Veanes, editors, Lpar-22. 22nd international conference on logic for programming, artificial intelligence and reasoning, volume 57 of EPiC Series in Computing, page 254–270. Easychair, 2018.
[Bibtex]
@inproceedings{LPAR-22:involutions_as_principal_types_application_as_unification_Analogy, author = {Alberto Ciaffaglione and Furio Honsell and Marina Lenisa and Ivan Scagnetto}, title = {The involutions-as-principal types/application-as-unification Analogy}, booktitle = {LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning}, editor = {Gilles Barthe and Geoff Sutcliffe and Margus Veanes}, series = {EPiC Series in Computing}, volume = {57}, pages = {254--270}, year = {2018}, publisher = {EasyChair}, bibsource = {EasyChair, https://easychair.org}, issn = {2398-7340}, url = {https://easychair.org/publications/paper/GRzV}, doi = {10.29007/ntwg}} - Alberto Ciaffaglione, Pietro Di Gianantonio, Furio Honsell, Marina Lenisa, and Ivan Scagnetto. Reversible computation and principal types in $\lambda$!-calculus. Logic and applications lap 2018, page 27, 2018.
[Bibtex]@article{ciaffaglione2018reversible, title={Reversible Computation and Principal Types in $\lambda$!-calculus}, author={Ciaffaglione, Alberto and Di Gianantonio, Pietro and Honsell, Furio and Lenisa, Marina and Scagnetto, Ivan}, journal={Logic and Applications LAP 2018}, pages={27}, year={2018} } - Alessio Mansutti and Marino Miculan. Deciding hedged bisimilarity. In Proceedings of ICTCS 2018, volume 2243 of CEUR Workshop Proceedings, page 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 } - Alessio Mansutti, Marino Miculan, and Marco Peressotti. Loose graph simulations. In Martina Seidl and Steffen Zschaler, editors, Software technologies: applications and foundations, page 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} }
2017
- Marino Miculan and Marco Peressotti. Reductions for transition systems at work: deriving a logical characterization of quantitative bisimulation. Corr, abs/1704.07181, 2017.
[Bibtex]
@article{DBLP:journals/corr/MiculanP17, author = {Marino Miculan and Marco Peressotti}, title = {Reductions for Transition Systems at Work: Deriving a Logical Characterization of Quantitative Bisimulation}, journal = {CoRR}, volume = {abs/1704.07181}, year = {2017}, url = {http://arxiv.org/abs/1704.07181}, archivePrefix = {arXiv}, eprint = {1704.07181}, timestamp = {Mon, 13 Aug 2018 16:46:27 +0200}, biburl = {https://dblp.org/rec/bib/journals/corr/MiculanP17}, bibsource = {dblp computer science bibliography, https://dblp.org} } - Furio Honsell, Luigi Liquori, Petar Maksimovic, and Ivan Scagnetto. LLF_P: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads. Logical Methods in Computer Science, {Volume 13, Issue 3}, 2017.
[Bibtex]
@article{lmcs:3771, Author = {Honsell, Furio and Liquori, Luigi and Maksimovic, Petar and Scagnetto, Ivan}, Doi = {10.23638/LMCS-13(3:2)2017}, Journal = {{Logical Methods in Computer Science}}, Keywords = {Computer Science - Logic in Computer Science ; F.4.1}, Month = Jul, Title = {{LLF_P: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads}}, Url = {http://lmcs.episciences.org/3771}, Volume = {{Volume 13, Issue 3}}, Year = {2017}, Bdsk-Url-1 = {http://lmcs.episciences.org/3771}, Bdsk-Url-2 = {https://dx.doi.org/10.23638/LMCS-13(3:2)2017}} - Claude Stolze, Luigi Liquori, Furio Honsell, and Ivan Scagnetto. Towards a logical framework with intersection and union types. In International workshop on logical frameworks and meta-languages lfmtp, page 1–9, 2017.
[Bibtex]@inproceedings{stolze2017towards, Author = {Stolze, Claude and Liquori, Luigi and Honsell, Furio and Scagnetto, Ivan}, Booktitle = {International Workshop on Logical Frameworks and Meta-languages LFMTP}, Pages = {1--9}, Title = {Towards a Logical Framework with Intersection and Union Types}, Year = {2017}} - Fabio Crestani, Stefano Mizzaro, and Ivan Scagnetto. Mobile information retrieval. SpringerBriefs in Computer Science. Springer international publishing, Gwerbestrasse 11, 6330 Cham, Switzerland, 1 edition, 2017.
[Bibtex]@book{Crestani2017, Address = {Gwerbestrasse 11, 6330 Cham, Switzerland}, Author = {Crestani, Fabio and Mizzaro, Stefano and Scagnetto, Ivan}, Edition = {1}, Isbn = {978-3-319-60776-4}, Price = {\$54.99}, Publisher = {Springer International Publishing}, Series = {SpringerBriefs in Computer Science}, Title = {Mobile Information Retrieval}, Year = {2017}} - Marco Pavan, Stefano Mizzaro, and Ivan Scagnetto. Mining movement data to extract personal points of interest: a feature based approach. In Cristian Lai, Alessandro Giuliani, and Giovanni Semeraro, editors, Information filtering and retrieval: dart 2014: revised and invited papers, page 35–61, Cham, 2017. Springer international publishing.
[Bibtex]
@inproceedings{Pavan2017, Abstract = {Due to the widespread of mobile devices in recent years, records of the locations visited by users are common and growing, and the availability of such large amounts of spatio-temporal data opens new challenges to automatically discover valuable knowledge. One aspect that is being studied is the identification of important locations, i.e. places where people spend a fair amount of time during their daily activities; we address it with a novel approach. Our proposed method is organised in two phases: first, a set of candidate stay points is identified by exploiting some state-of-the-art algorithms to filter the GPS-logs; then, the candidate stay points are mapped onto a feature space having as dimensions the area underlying the stay point, its intensity (e.g. the time spent in a location) and its frequency (e.g. the number of total visits). We conjecture that the feature space allows to model aspects/measures that are more semantically related to users and better suited to reason about their similarities and differences than simpler physical measures (e.g. latitude, longitude, and timestamp). An experimental evaluation on the GeoLife public dataset confirms the effectiveness of our approach and sheds some light on the peculiar features and critical issues of location based systems.}, Address = {Cham}, Author = {Pavan, Marco and Mizzaro, Stefano and Scagnetto, Ivan}, Booktitle = {Information Filtering and Retrieval: DART 2014: Revised and Invited Papers}, Doi = {10.1007/978-3-319-46135-9_3}, Editor = {Lai, Cristian and Giuliani, Alessandro and Semeraro, Giovanni}, Isbn = {978-3-319-46135-9}, Pages = {35--61}, Publisher = {Springer International Publishing}, Title = {Mining Movement Data to Extract Personal Points of Interest: A Feature Based Approach}, Url = {https://doi.org/10.1007/978-3-319-46135-9_3}, Year = {2017}, Bdsk-Url-1 = {https://doi.org/10.1007/978-3-319-46135-9_3}} - 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}, Date-Modified = {2017-11-30 09:12:53 +0000}, Pages = {126-137}, Pdf = {http://ceur-ws.org/Vol-1949/ICTCSpaper11.pdf}, Series = {CEUR-WS}, Title = {Deciding Weak Weighted Bisimulation}, Volume = 1849, 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, Author = {Miculan, Marino and Peressotti, Marco}, Journal = {arXiv preprint arXiv:1704.07181}, Title = {Reductions for Transition Systems at Work: Deriving a Logical Characterization of Quantitative Bisimulation}, Year = {2017}} - Alessio Mansutti, Marino Miculan, and Marco Peressotti. Loose graph simulations. In Proceedings of GCM 2017, 2017.
[Bibtex]
@inproceedings{mansutti2017loose, Author = {Mansutti, Alessio and Miculan, Marino and Peressotti, Marco}, Booktitle = {Proceedings of {GCM} 2017}, Pdf = {https://arxiv.org/pdf/1705.08241}, Title = {Loose Graph Simulations}, Year = 2017} - Marino Miculan and Florian Rabe, editors. LFMTP ’17: proceedings of the workshop on logical frameworks and meta-languages: theory and practiceAcm, 2017.
[Bibtex]
@proceedings{Miculan:2017:3130261, Editor = {Miculan, Marino and Rabe, Florian}, Isbn = {978-1-4503-5374-8}, Location = {Oxford, United Kingdom}, Publisher = {ACM}, Title = {{LFMTP} '17: Proceedings of the Workshop on Logical Frameworks and Meta-Languages: Theory and Practice}, Url = {http://dl.acm.org/citation.cfm?id=3130261}, Year = {2017}, Bdsk-Url-1 = {http://dl.acm.org/citation.cfm?id=3130261}}
2016
- Furio Honsell, Marina Lenisa, Luigi Liquori, and Ivan Scagnetto. Implementing cantor’s paradise. In Atsushi Igarashi, editor, Programming languages and systems: 14th asian symposium, aplas 2016, hanoi, vietnam, november 21 – 23, 2016, proceedings, page 229–250, Cham, 2016. Springer international publishing.
[Bibtex]
@inproceedings{Honsell2016, Abstract = {Set-theoretic paradoxes have made all-inclusive self-referential Foundational Theories almost a taboo. The few daring attempts in the literature to break this taboo avoid paradoxes by restricting the class of formul{\ae} allowed in Cantor's na{\"\i}ve Comprehension Principle. A different, more intensional approach was taken by Fitch, reformulated by Prawitz, by restricting, instead, the shape of deductions, namely allowing only normal(izable) deductions. The resulting theory is quite powerful, and consistent by design. However, modus ponens and Scotus ex contradictione quodlibet principles fail. We discuss Fitch-Prawitz Set Theory ( {\$}{\$}{\backslash}mathsf {\{}FP{\}}{\$}{\$} ) and implement it in a Logical Framework with so-called locked types, thereby providing a ``Computer-assisted Cantor's Paradise'': an interactive framework that, unlike the familiar Coq and Agda, is closer to the familiar informal way of doing mathematics by delaying and consolidating the required normality tests. We prove a Fixed Point Theorem, whereby all partial recursive functions are definable in {\$}{\$}{\backslash}mathsf {\{}FP{\}}{\$}{\$} . We establish an intriguing connection between an extension of {\$}{\$}{\backslash}mathsf {\{}FP{\}}{\$}{\$} and the Theory of Hyperuniverses: the bisimilarity quotient of the coalgebra of closed terms of {\$}{\$}{\backslash}mathsf {\{}FP{\}}{\$}{\$} satisfies the Comprehension Principle for Hyperuniverses.}, Address = {Cham}, Author = {Honsell, Furio and Lenisa, Marina and Liquori, Luigi and Scagnetto, Ivan}, Booktitle = {Programming Languages and Systems: 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21 - 23, 2016, Proceedings}, Doi = {10.1007/978-3-319-47958-3_13}, Editor = {Igarashi, Atsushi}, Isbn = {978-3-319-47958-3}, Pages = {229--250}, Publisher = {Springer International Publishing}, Title = {Implementing Cantor's Paradise}, Url = {https://doi.org/10.1007/978-3-319-47958-3_13}, Year = {2016}, Bdsk-Url-1 = {https://doi.org/10.1007/978-3-319-47958-3_13}} - Alessio Mansutti and Marino Miculan. Deciding hedged bisimilarity. Corr, abs/1611.03424, 2016.
[Bibtex]
@article{DBLP:journals/corr/MansuttiMiculan16, Author = {Alessio Mansutti and Marino Miculan}, Journal = {CoRR}, Title = {Deciding Hedged Bisimilarity}, Url = {http://arxiv.org/abs/1611.03424}, Volume = {abs/1611.03424}, Year = {2016}, Bdsk-Url-1 = {http://arxiv.org/abs/1611.03424}} - 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}, Pages = {88-102}, Pdf = {http://ceur-ws.org/Vol-1720/full7.pdf}, Series = {CEUR-WS}, Title = {On the bisimulation hierarchy of state-to-function transition systems}, Volume = 1720, 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}, Pages = {203-220}, Pdf = {http://ceur-ws.org/Vol-1720/full15.pdf}, Series = {CEUR-WS}, Title = {Disjunctive Probabilistic Modal Logic is Enough for Bisimilarity on Reactive Probabilistic Systems}, Url = {https://arxiv.org/abs/1601.06198}, Volume = 1720, Year = 2016, Bdsk-Url-1 = {https://arxiv.org/abs/1601.06198}} - 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}, Number = 1, Series = {International Journal of Electronic Governance}, Title = {Special Issue on Methodologies, Technologies and Tools Enabling e-Government}, Url = {http://www.inderscience.com/info/inarticletoc.php?jcode=ijeg&year=2016&vol=8&issue=1}, Volume = 8, Year = 2016, Bdsk-Url-1 = {http://www.inderscience.com/info/inarticletoc.php?jcode=ijeg&year=2016&vol=8&issue=1}} - 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}, Bibsource = {dblp computer science bibliography, http://dblp.org}, Biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/MiculanP16}, Journal = {CoRR}, Timestamp = {Tue, 01 Mar 2016 17:47:25 +0100}, Title = {A Specification of Open Transactional Memory for {Haskell}}, Url = {http://arxiv.org/abs/1602.05365}, Volume = {abs/1602.05365}, Year = {2016}, Bdsk-Url-1 = {http://arxiv.org/abs/1602.05365}} - 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, 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. }, Author = {Marino Miculan and Marco Peressotti}, Doi = {10.1016/j.tcs.2016.01.012}, Issn = {0304-3975}, Journal = {Theoretical Computer Science}, Keywords = {Quantitative models}, Pages = {135-154}, Title = {Structural operational semantics for non-deterministic processes with quantitative aspects}, Url = {http://www.sciencedirect.com/science/article/pii/S0304397516000232}, Volume = {655}, Year = {2016}, Bdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/S0304397516000232}, Bdsk-Url-2 = {https://dx.doi.org/10.1016/j.tcs.2016.01.012}}
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]
@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, page 213–229, 2015.
[Bibtex]
@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]
@article{bmp:jlamp15, 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. }, Author = {Tomasz Brengos and Marino Miculan and Marco Peressotti}, Doi = {10.1016/j.jlamp.2015.09.002}, Issn = {2352-2208}, Journal = {Journal of Logical and Algebraic Methods in Programming}, Keywords = {Saturation semantics}, Pages = {-}, Pdf = {http://arxiv.org/pdf/1411.0090v3}, Title = {Behavioural equivalences for coalgebras with unobservable moves}, Url = {http://arxiv.org/abs/1411.0090}, Year = {2015}, Bdsk-Url-1 = {http://arxiv.org/abs/1411.0090}, Bdsk-Url-2 = {https://dx.doi.org/10.1016/j.jlamp.2015.09.002}} - 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]
@incollection{mps:air15, Author = {Mizzaro, Stefano and Pavan, Marco and Scagnetto, Ivan}, Booktitle = {Advances in Information Retrieval}, Doi = {10.1007/978-3-319-16354-3_56}, Editor = {Hanbury, Allan and Kazai, Gabriella and Rauber, Andreas and Fuhr, Norbert}, Isbn = {978-3-319-16353-6}, Language = {English}, Pages = {507-512}, Publisher = {Springer International Publishing}, Series = {Lecture Notes in Computer Science}, Title = {Content-Based Similarity of Twitter Users}, Url = {http://dx.doi.org/10.1007/978-3-319-16354-3_56}, Volume = {9022}, Year = {2015}, Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-319-16354-3_56}} - Alberto Ciaffaglione and Ivan Scagnetto. Mechanizing type environments in weak hoas. Theoretical computer science, page -, 2015.
[Bibtex]
@article{Ciaffaglione2015, 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. }, Author = {Alberto Ciaffaglione and Ivan Scagnetto}, Doi = {http://dx.doi.org/10.1016/j.tcs.2015.07.019}, Issn = {0304-3975}, Journal = {Theoretical Computer Science}, Keywords = {POPLmark challenge}, Pages = {-}, Title = {Mechanizing type environments in weak HOAS}, Url = {http://www.sciencedirect.com/science/article/pii/S0304397515006404}, Year = {2015}, Bdsk-Url-1 = {http://www.sciencedirect.com/science/article/pii/S0304397515006404}, Bdsk-Url-2 = {http://dx.doi.org/10.1016/j.tcs.2015.07.019}} - Furio Honsell, Luigi Liquori, Petar Maksimovic, 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]
@inproceedings{EPTCS185.1, Author = {Honsell, Furio and Liquori, Luigi and Maksimovic, Petar and Scagnetto, Ivan}, Booktitle = {Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, Berlin, Germany, 1 August 2015}, Date-Modified = {2017-11-30 09:15:03 +0000}, Doi = {10.4204/EPTCS.185.1}, Editor = {Cervesato, Iliano and Chaudhuri, Kaustuv}, Pages = {3-17}, Publisher = {Open Publishing Association}, Series = {Electronic Proceedings in Theoretical Computer Science}, Title = {Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks}, Volume = {185}, Year = {2015}, Bdsk-Url-1 = {https://dx.doi.org/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]
@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, page 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}} - 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]
@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, page 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, page 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} - 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]
@incollection{hls:mfcs14, Author = {Honsell, Furio and Liquori, Luigi and Scagnetto, Ivan}, Booktitle = {Mathematical Foundations of Computer Science 2014}, Doi = {10.1007/978-3-662-44522-8_28}, Editor = {Csuhaj-Varj{\'u}, Erzs{\'e}bet and Dietzfelbinger, Martin and {\'E}sik, Zolt{\'a}n}, Isbn = {978-3-662-44521-1}, Language = {English}, Pages = {327-339}, Publisher = {Springer Berlin Heidelberg}, Series = {Lecture Notes in Computer Science}, Title = {{LaxF}: Side Conditions and External Evidence as Monads}, Url = {http://dx.doi.org/10.1007/978-3-662-44522-8_28}, Volume = {8634}, Year = {2014}, Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-662-44522-8_28}} - 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]
@inproceedings{Ciaffaglione:2014:IAB:2631172.2631180, Acmid = {2631180}, Address = {New York, NY, USA}, Articleno = {8}, Author = {Ciaffaglione, Alberto and Scagnetto, Ivan}, Booktitle = {Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice}, Doi = {10.1145/2631172.2631180}, Isbn = {978-1-4503-2817-3}, Keywords = {Higher-Order Abstract Syntax, Logical Frameworks, Type Theory}, Location = {Vienna, Austria}, Numpages = {8}, Pages = {8:1--8:8}, Publisher = {ACM}, Series = {LFMTP '14}, Title = {Internal Adequacy of Bookkeeping in Coq}, Url = {http://doi.acm.org/10.1145/2631172.2631180}, Year = {2014}, Bdsk-Url-1 = {http://doi.acm.org/10.1145/2631172.2631180}, Bdsk-Url-2 = {https://dx.doi.org/10.1145/2631172.2631180}} - 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, page 57–62, New York, NY, USA, 2014. Acm.
[Bibtex]
@inproceedings{Mizzaro:2014:STC:2632188.2632205, Acmid = {2632205}, Address = {New York, NY, USA}, Author = {Mizzaro, Stefano and Pavan, Marco and Scagnetto, Ivan and Valenti, Martino}, Booktitle = {Proceedings of the First International Workshop on Social Media Retrieval and Analysis}, Doi = {10.1145/2632188.2632205}, Isbn = {978-1-4503-3022-0}, Keywords = {context-aware retrieval, enrichment, evaluation, wikipedia}, Location = {Gold Coast, Queensland, Australia}, Numpages = {6}, Pages = {57--62}, Publisher = {ACM}, Series = {SoMeRA '14}, Title = {Short Text Categorization Exploiting Contextual Enrichment and External Knowledge}, Url = {http://doi.acm.org/10.1145/2632188.2632205}, Year = {2014}, Bdsk-Url-1 = {http://doi.acm.org/10.1145/2632188.2632205}, Bdsk-Url-2 = {https://dx.doi.org/10.1145/2632188.2632205}} - 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, page 18–25, New York, NY, USA, 2014. Acm.
[Bibtex]
@inproceedings{Mizzaro:2014:CRS:2601301.2601305, Acmid = {2601305}, Address = {New York, NY, USA}, Author = {Mizzaro, Stefano and Pavan, Marco and Scagnetto, Ivan and Zanello, Ivano}, Booktitle = {Proceedings of the 4th Workshop on Context-Awareness in Retrieval and Recommendation}, Doi = {10.1145/2601301.2601305}, Isbn = {978-1-4503-2723-7}, Keywords = {apps, context-aware retrieval, evaluation, mobile, ranking, recommender systems}, Location = {Amsterdam, The Netherlands}, Numpages = {8}, Pages = {18--25}, Publisher = {ACM}, Series = {CARR '14}, Title = {A Context-aware Retrieval System for Mobile Applications}, Url = {http://doi.acm.org/10.1145/2601301.2601305}, Year = {2014}, Bdsk-Url-1 = {http://doi.acm.org/10.1145/2601301.2601305}, Bdsk-Url-2 = {https://dx.doi.org/10.1145/2601301.2601305}}
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}} - Furio Honsell, Marina Lenisa, Ivan Scagnetto, Luigi Liquori, and Petar Maksimovic. An open logical framework. Journal of logic and computation, 2013.
[Bibtex]
@article{Honsell31072013, 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{\'e} 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.}, Author = {Honsell, Furio and Lenisa, Marina and Scagnetto, Ivan and Liquori, Luigi and Maksimovic, Petar}, Doi = {10.1093/logcom/ext028}, Eprint = {http://logcom.oxfordjournals.org/content/early/2013/07/31/logcom.ext028.full.pdf+html}, Journal = {Journal of Logic and Computation}, Title = {An open logical framework}, Url = {http://logcom.oxfordjournals.org/content/early/2013/07/31/logcom.ext028.abstract}, Year = {2013}, Bdsk-Url-1 = {http://logcom.oxfordjournals.org/content/early/2013/07/31/logcom.ext028.abstract}, Bdsk-Url-2 = {https://dx.doi.org/10.1093/logcom/ext028}}
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, page 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} - 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., page 109–124, 2012.
[Bibtex]
@inproceedings{DBLP:journals/corr/abs-1303-7332, Author = {Alberto Ciaffaglione and Ivan Scagnetto}, Bibsource = {dblp computer science bibliography, http://dblp.org}, Biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1303-7332}, Booktitle = {Proceedings Seventh Workshop on Logical and Semantic Frameworks, with Applications, {LSFA} 2012, Rio de Janeiro, Brazil, September 29-30, 2012.}, Crossref = {DBLP:journals/corr/abs-1303-7136}, Doi = {10.4204/EPTCS.113.11}, Pages = {109--124}, Timestamp = {Sun, 15 Mar 2015 09:37:18 +0100}, Title = {A weak {HOAS} approach to the POPLmark Challenge}, Url = {http://dx.doi.org/10.4204/EPTCS.113.11}, Year = {2012}, Bdsk-Url-1 = {http://dx.doi.org/10.4204/EPTCS.113.11}} - 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, page 13–22, New York, NY, USA, 2012. Acm.
[Bibtex]
@inproceedings{Honsell:2012:LPL:2364406.2364409, Acmid = {2364409}, Address = {New York, NY, USA}, Author = {Honsell, Furio and Lenisa, Marina and Liquori, Luigi and Maksimovic, Petar and Scagnetto, Ivan}, Booktitle = {Proceedings of the Seventh International Workshop on Logical Frameworks and Meta-languages, Theory and Practice}, Doi = {10.1145/2364406.2364409}, Isbn = {978-1-4503-1578-4}, Keywords = {logical frameworks, type theory}, Location = {Copenhagen, Denmark}, Numpages = {10}, Pages = {13--22}, Publisher = {ACM}, Series = {LFMTP '12}, Title = {LFP: A Logical Framework with External Predicates}, Url = {http://doi.acm.org/10.1145/2364406.2364409}, Year = {2012}, Bdsk-Url-1 = {http://doi.acm.org/10.1145/2364406.2364409}, Bdsk-Url-2 = {https://dx.doi.org/10.1145/2364406.2364409}}
2011
- Marino Miculan and Caterina Urban. Formal analysis of Facebook Connect single sign-on authentication protocol. In SofSem 2011, proceedings of student research forum, page 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}} - 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, 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}, Number = {1}, Pages = {38--47}, Publisher = {IEEE}, Title = {The context-aware browser}, Volume = {25}, Year = {2010}} - 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]
@incollection{cab2010, 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}, Booktitle = {Pervasive Computing}, Doi = {10.1007/978-1-84882-599-4_8}, Editor = {Hassanien, Aboul-Ella and Abawajy, Jemal H. and Abraham, Ajith and Hagras, Hani}, Isbn = {978-1-84882-598-7}, Keywords = {Context-aware browser; CAB; MoBe; Mobile; Bayesian; Inference and wireless systems}, Language = {English}, Pages = {157-180}, Publisher = {Springer London}, Series = {Computer Communications and Networks}, Title = {AI Techniques in a Context-Aware Ubiquitous Environment}, Url = {http://dx.doi.org/10.1007/978-1-84882-599-4_8}, Year = {2010}, Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-1-84882-599-4_8}}
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}, Bdsk-Url-2 = {https://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, page 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 ScienceSpringer, 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} - 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), page 668–672, Amsterdam – NLD, 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)}, Date-Modified = {2017-11-30 09:12:22 +0000}, Location = {Patras, Greece}, Month = {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, page 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, page 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
- 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}
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} - 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}