print · login   

Working Groups

EUTypes is organised into four Working Groups.

WG1: Theoretical Foundations

Type theory as a foundational language for expressing concepts from computer science and mathematics with the specific aim to improve programming and to enhance the certification of computer systems.

Chair: Prof Andrej Bauer, University of Ljubljana, Slovenia

WG2: Type-theoretic tools

Modern type theories form the basis of sophisticated platforms that integrate specification and programming with methodologies and tools for the verification of programs.

Chair: Dr Assia Mahboubi, INRIA Paris, France

During the time frame of the action, many experiments have been carried regarding the implementation of type theoretic methods. These experiments can be broadly classified in three categories:

  • implementing new proof assistants, for new variants of type theory. Notable examples:

Andromeda, Arend developed at JetBrains, Lean, mainly developed at Microsoft Research

  • conducting important changes in existing proof assistants, e.g. experimenting with the implementation of definitional proof irrelevance in Coq, or the elaboration of dependent

pattern matching in Agda.

  • implementing new large scale libraries inside proof assistants

Metacoq, UniMath, Mathematical Components, mathlib.

Highlights:

2017)

WG3: Types for programming

Type-based programming increases the security, reliability, resilience and reusability of software as evidenced by the increasingly popularity of strongly typed languages and the widespread use of types in applied programming language research.

Chair: Dr Andreas Abel, Chalmers University Gothenburg, Sweden

WG4: Types for verification

The study and development of type based verification systems aims at expressing and optimising the verification tasks in terms of existing strong type systems such as the Calculus of Inductive Constructions, Martin-Löf type theory or Higher-Order Logic.

The research objective of WG4 is type-based verification of software systems. In this contextual framework, the working group has addressed both verification of concrete software systems as well as the "meta-problem" of devising novel tools for conducting such verification, thereby making it easier to verify software systems in the future.

A good examples of verification work on a concrete system is the result of Almeida et al., who provide a machine-checked proof of the security of the key management service within the Amazon Web Services (AWS).

Developing new tools is important - if we want to reach a broader practical availability of provably secure software, better tools are required to automate the otherwise tedious formal verification work. This structural objective has also motivated the Meta-F* and Iris, which provide new programming languages where verification is the first-class citizen of the languages.

Chair: Dr Keiko Nakata, SAP Potsdam, Germany

WG4 research output

Selected Publications

  • Annenkov, D., Nielsen, J. B. & Spitters, B. (2020) ConCert: a smart contract certification framework in Coq. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020 (pp. 215--228). https://doi.org/10.1145/3372885.3373829
  • Rodrigues, V., Donetti, S. & Damiani, F. (2019) Certifying delta-oriented programs. Volume 18, Number 5 (pp. 2875--2906).
  • Mirko Spasić, Milena Vujošević Janičić. Verification Supported Refactoring of Embedded SQL. Software Quality Journal, Springer. (2020)
  • Andrici, C.-C. & Ciobaca, S. (2019) Verifying the DPLL Algorithm in Dafny. In Proceedings Third Symposium on Working Formal Methods, FROM 2019, Timişoara, Romania, 3-5 September 2019 (pp. 3 -- 15).
  • Nanevski, A., Banerjee, A., Delbianco, G. A. & Fábregas, I. (2019) Specifying concurrent programs in separation logic: morphisms and simulations. In Proceedings of the ACM on Programming Languages, Volume 3, Number OOPSLA (pp. 161:1--161:30).
  • Alessi, F., Ciaffaglione, A., Di Gianantonio, P., Honsell, F., & Lenisa, M. (2019) A Definitional Implementation of the Lax Logical Framework LLFP in Coq, for Supporting Fast and Loose Reasoning. In Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@LICS 2019, Vancouver, Canada, 22nd June 2019 (pp. 8--23).
  • D. Firsov, A. Buldas, A. Truu, R. Laanoja. Verified security of BLTs signature scheme. In Proc. of 9th ACM SIGPLAN Int. Conf. on Certified Programs and Proofs, CPP 2020 (New Orleans, LA, Jan. 2020), pp. 244-257. ACM Press, 2020.
  • Miroslav Popovic, Marko Popovic, Silvia Ghilezan, Branislav Kordic. Formal Verification of Python Software Transactional Memory Serializability Based on the Push/Pull Semantic Model. European Conference on the Engineering of Computer Based Systems ECBS 2019:6:1-6:8
  • G. Martínez, D. Ahman, V. Dumitrescu, N. Giannarakis, C. Hawblitzel, C. Hritcu, M. Narasimhamurthy, Z. Paraskevopoulou, C. Pit-Claudel, J. Protzenko, T. Ramananandro, A. Rastogi, N. Swamy. Meta-F*: proof automation with SMT, tactics, and metaprograms. In L. Caires, ed., Proc. of 28th Europ. Symp. on Programming, ESOP 2019 (Prague, Apr. 2019), v. 11423 of Lect. Notes in Comput. Sci., pp. 30-59. Springer, 2019.
  • Larchey-Wendling D., Matthes R. (2019) Certification of Breadth-First Algorithms by Extraction. In: Hutton G. (eds) Mathematics of Program Construction. MPC 2019. Lecture Notes in Computer Science, vol 11825. Springer, Cham
  • José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, and Serdar Tasiran. A Machine-Checked Proof of Security for AWS Key Management Service. In ACM CCS 2019 - 26th ACM Conference on Computer and Communications Security, volume 16, pages 63–78, London, United Kingdom, November 2019. ACM Press.
  • Dan Frumin, Robbert Krebbers and Lars Birkedal. Compositional Non-Interference for Fine-Grained Concurrent Programs. To appear in Security & Privacy 2021.