Nominal Structural Operational Semantics
Operational semantics is a widely-used methodology to define formal
semantics for computer languages, which represents the execution of
programs as step-by-step development of an abstract
machine. Structural Operational Semantics (SOS) is a logical and
structural approach to defining operational semantics, which, in the
light of its intuitive appeal and flexibility, has become the de
facto standard for defining operational semantics.
This project will focus on one of the crucial aspects in the
definition of semantic models for programming and specification
languages that has not yet been addressed satisfactorily within the
framework of the theory of SOS, i.e., the treatment of concepts such
as variables, names and binders. The work will be based on the
framework of Nominal SOS, which has recently been developed by some of
the proposers. The overarching aim of the project is to bring the
framework of Nominal SOS to a level of maturity that is comparable to
that of the standard theory of SOS, and to establish firmly Nominal
SOS as a framework of choice for the study and the development of the
theory of languages with first-class notions of names and binders.
Icelandic Research Fund Project nr. 141558-041 (2014-2016)
The research team at Reykjavik University includes Luca Aceto (PI),
Ignacio Fabregas (postdoctoral researcher), Alvaro Garcia-Perez
(postdoctoral researcher) and Anna Ingolfsdottir
(co-PI). Matteo Cimini (Indiana
University, Center for Research in Extreme Scale Technologies, USA) is
an external collaborator on the project.
Accepted and published papers
Books and edited volumes
- Luca Aceto and David de Frutos Escrig
of the 26th International Conference on Concurrency Theory (CONCUR
2015). ISBN 978-3-939897-91-0, LIPICS Vol. 42, September
- L. Aceto, I. Fabregas, A. Garcia-Perez and
of the 27th Nordic Workshop on Programming Theory, NWPT 2015.
Technical Report RUTR-SCS16001, School of Computer Science,
Reykjavik University, February 2016.
- Luca Aceto, Alvaro Garcia Perez and Anna
Ingolfsdottir. Rule formats for bounded
nondeterminism in structural operational
semantics. In Semantics, Logics, and Calculi --- Essays
Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion
of Their 60th Birthdays (Christian W. Probst, Chris Hankin and
Rene Rydhof Hansen eds.), Lecture Notes in Computer Science 9560,
pp. 313-343, Springer 2016. The publisher's version of the paper is
- Alvaro Garcia Perez and Pablo
Noguera. No solvable
lambda-value term left behind. To appear in
Logical Methods in
Computer Science, 2016.
- Luca Aceto, Dario Della Monica, Ignacio Fabregas and Anna
Ingolfsdottir. When are prime formulae
characteristic?. Proceedings of MFCS 2015, Part 1, Lecture Notes in
Computer Science 9234, pages 76-88, Springer Verlag, August 2015.
- L. Aceto, I. Fabregas, C. Gregorio-Rodriguez
and A. Ingolfsdottir. Logical characterisations and
compositionality of input-output conformance simulation. To appear
in the Proceedings of the 43rd International Conference on
Current Trends in Theory and Practice of Computer Science, SOFSEM
2017, Foundations Of Computer Science Track, Lecture Notes in
Computer Science, Springer, January 2017.
- L. Aceto, K.G. Larsen, A. Morichetta and
F. Tiezzi. A cost/reward method for
optimal infinite scheduling in Mobile Cloud Computing.
Proceedings of the 12th International Conference on Formal
Aspects of Components Software (FACS 2015), Lecture Notes in
Computer Science, Springer, 2015.
- L. Aceto, A. Morichetta and
F. Tiezzi. Decision Support for Mobile Cloud
Computing Applications via Model Checking. Proceedings of
IEEE Mobile Cloud 2015, the 3rd IEEE International Conference on
Mobile Cloud Computing, Services, and Engineering. Pages
199-204. IEEE Computer Society, 2015.
- Adrian Francalanza, Luca Aceto and Anna Ingolfsdottir.
On Verifying Hennessy-Milner Logic
with Recursion at Runtime. Proceedings of RV 2015, Lecture Notes in
Computer Science 9333, pages 71-86, Springer Verlag, September 2015.
- Luca Aceto and David de Frutos
for the special issue of Acta Informatica devoted to selected papers
from CONCUR 2015. Acta Informatica, Springer, February 2017.
- Luca Aceto,
Ignacio Fábregas, Alvaro García-Pérez and Anna Ingólfsdóttir. A unified rule format for bounded
nondeterminism in SOS with terms as labels. Submitted for journal publication.
Papers that are about to be submitted
- Luca Aceto, Matteo Cimini, Anna Ingolfsdottir, MohammadReza
Mousavi, Michel A. Reniers and Murdoch
J. Gabbay. Nominal Structural Operational
Semantics. Draft paper for journal submission.
- Álvaro García-Pérez, Pablo Nogueira and Pierre-Yves Strub. On
closure calculi and the full-reducing Krivine machine. Conference
paper to be submitted to the First International Conference on Formal
Structures for Computation and Deduction (FSCD'16).
- Kari Tristan Helgason. Runtime
Verification with DetectEr: a case study. Undergraduate research
opportunity article at Reykjavik University. May 2015.
- Sævar Örn Kjartansson. The expressive power of
deterministic monitors for muHML. Research-based BSc thesis in the
Discrete Mathematics and Computer Science programme at Reykjavik
University. December 2015.
Papers in preparation
- Luca Aceto, Matteo Cimini, Anna Ingolfsdottir, MohammadReza Mousavi
and Michel A. Reniers. A Congruence Format for Calculi with Binders in
Nominal SOS. Working draft paper for conference and journal