Post-Proceedings TYPES 2021

Publications Accepted to Post-Proceedings in LIPIcs Volume 239

The complete volume can be found via the DOI 10.4230/LIPIcs.TYPES.2021. The individual publications are as follows.

Foreword

This volume constitutes the post-proceedings of the 27th International Conference on Types for Proofs and Programs, TYPES 2021, that was held virtually from 14 to 18 June 2021 with organisation based in Leiden. The TYPES meetings are a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalised and computer assisted reasoning and computer programming. The meetings from 1990 to 2008 were annual workshops of a sequence of five EU-funded networking projects. Since 2009, TYPES has been run as an independent conference series. Previous TYPES meetings were held in Antibes (1990), Edinburgh (1991), Båstad (1992), Nijmegen (1993), Båstad (1994), Torino (1995), Aussois (1996), Kloster Irsee (1998), Lökeberg (1999), Durham (2000), Berg en Dal near Nijmegen (2002), Torino (2003), Jouy-en-Josas near Paris (2004), Nottingham (2006), Cividale del Friuli (2007), Torino (2008), Aussois (2009), Warsaw (2010), Bergen (2011), Toulouse (2013), Paris (2014), Tallinn (2015), Novi Sad (2016), Budapest (2017), Braga (2018), Oslo (2019) and Turin (2020). The TYPES areas of interest include, but are not limited to: Foundations of type theory and constructive mathematics; Homotopy type theory; Applications of type theory; Dependently typed programming; Industrial uses of type theory technology; Meta-theoretic studies of type systems; Proof assistants and proof technology; Automation in computer-assisted reasoning; Links between type theory and functional programming; Formalizing mathematics using type theory; Type theory in linguistics. The TYPES conferences are of open and informal character. Selection of contributed talks is based on short abstracts; reporting work in progress and work presented or published elsewhere is welcome. A formal post-proceedings volume is prepared after the conference; papers submitted to that volume must represent unpublished work and are subjected to a full peer-review process.

Already in 2020, TYPES could not take place due to the situation surrounding SARS-CoV-2 and this very same situation forced us to make TYPES 2021 a virtual event. Given these circumstances and the general impact of measures taken in reaction to SARS-CoV-2, the conference and this volume can be considered a relative success. The conference programme consisted of four invited talks by Ulrik Buchholtz, Stephanie Balzer, Sara Negri and Pierre-Marie Pédrot. For a virtual event, the participation in the conference was high with 44 contributed talks, and 160 registered and about 70 active participants. The abstracts can be downloaded from the page of Accepted Contributions.

Even though the circumstances were not ideal, we were able to strengthen the link between the conference and these post-proceedings by giving more room for discussion during the conference of work that the authors intended to submit to the post-proceedings. Indeed, initially 23 papers were submitted to the post-proceedings, out of which 8 were retracted. However, we are happy to ultimately have post-proceedings consisting of 12 high-quality papers on formalised mathematics and semantics, foundations of type theory, geometric and linear logic, categorical methods in type theory, and types for processes. We thank all the authors and reviewers for their hard work to make this possible! Finally, we would like to thank the Leiden Institute of Advanced Computer Science for kindly covering the costs of the conference and the post-proceedings. This simplified participation given the virtual setup greatly! For the future, we hope that TYPES is not forced to be held again virtually, even though virtual attendance to talks is an interesting option to have, and the most important elements of TYPES can be brought back: discussion and spontaneous interaction!


Henning Basold, Jesper Cockx and Silvia Ghilezan, June 2022.