Nominal Structural Operational Semantics
Icelandic Research Fund Project nr. 141558-041 (2014-2016)
Status: Ongoing

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.

Researchers

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.

Publications

Accepted and published papers

Books and edited volumes

  1. Luca Aceto and David de Frutos Escrig (Eds.). Proceedings of the 26th International Conference on Concurrency Theory (CONCUR 2015). ISBN 978-3-939897-91-0, LIPICS Vol. 42, September 2015.
  2. Luca Aceto and David de Frutos Escrig. Special Issue: Selected papers from the 26th International Conference on Concurrency Theory (CONCUR 2015), Acta Informatica 54(1):1--125, February 2017.
  3. Luca Aceto and David de Frutos Escrig. Special Issue: Selected papers from the 26th International Conference on Concurrency Theory (CONCUR 2015), Acta Informatica 54(2):127-242, March 2017.
  4. Luca Aceto and David de Frutos Escrig. Special Issue: Selected papers from the 26th International Conference on Concurrency Theory (CONCUR 2015), Acta Informatica 54(3):243--341, May 2017.
  5. L. Aceto, I. Fabregas, A. Garcia-Perez and A. Ingolfsdottir. Proceedings of the 27th Nordic Workshop on Programming Theory, NWPT 2015. Technical Report RUTR-SCS16001, School of Computer Science, Reykjavik University, February 2016.

Book chapters

  1. 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 here.

Journal papers

  1. 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. Journal of Logical and Algebraic Methods in Programming, 2017. To appear.
  2. Alvaro Garcia Perez and Pablo Noguera. No solvable lambda-value term left behind. Logical Methods in Computer Science 12(2), 2016.

Conference papers

  1. 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.
  2. Luca Aceto, Ignacio Fábregas, Alvaro García-Pérez, Anna Ingólfsdóttir and Yolanda Ortega-Mallen. Rule Formats for Nominal Process Calculi. To appear in the Proceedings of CONCUR 2017, the 28th International Conference on Concurrency Theory, 5-8 September 2017, Berlin, Germany. LIPIcs, September 2017.
  3. 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.
  4. 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.
  5. 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.
  6. 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.

Other publications

  1. Luca Aceto and David de Frutos Escrig. Foreword for the special issue of Acta Informatica devoted to selected papers from CONCUR 2015. Acta Informatica, Springer, February 2017.

Submitted papers

  1. None at this time.

Papers that are about to be submitted

  1. Luca Aceto, Matteo Cimini, Anna Ingolfsdottir, MohammadReza Mousavi, Michel A. Reniers and Murdoch J. Gabbay. Nominal Structural Operational Semantics. Draft paper for journal submission.
  2. Á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).

Student theses

  1. Kari Tristan Helgason. Runtime Verification with DetectEr: a case study. Undergraduate research opportunity article at Reykjavik University. May 2015.
  2. 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

  1. 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 submission.