Published: 8th April 2022
DOI: 10.4204/EPTCS.357
ISSN: 2075-2180


Proceedings 16th
Logical and Semantic Frameworks with Applications
Buenos Aires, Argentina (Online), 23rd - 24th July, 2021

Edited by: Mauricio Ayala-Rincon and Eduardo Bonelli

Mauricio Ayala-Rincón and Eduardo Bonelli
A Quick Overview on the Quantum Control Approach to the Lambda Calculus
Alejandro Díaz-Caro
A Note on Confluence in Typed Probabilistic Lambda Calculi
Rafael Romero and Alejandro Díaz-Caro
About Opposition and Duality in Paraconsistent Type Theory
Juan C. Agudelo-Agudelo and Andrés Sicard-Ramírez
SeCaV: A Sequent Calculus Verifier in Isabelle/HOL
Asta Halkjær From, Frederik Krogsdal Jacobsen and Jørgen Villadsen
On Logics of Perfect Paradefinite Algebras
Joel Gomes, Vitor Greati, Sérgio Marcelino, João Marcos and Umberto Rivieccio
GADTs, Functoriality, Parametricity: Pick Two
Patricia Johann, Enrico Ghiorzi and Daniel Jeffries
A Subexponential View of Domains in Session Types
Daniele Nantes, Carlos Olarte and Daniel Ventura


This volume contains the post-proceedings of the Sixteenth Logical and Semantic Frameworks with Applications (LSFA 2021). The meeting was held online on July 23-24, 2021, organised by the Universidad de Buenos Aires, Argentina. LSFA started in 2006 in Natal (LSFA06), and its second and third editions were held in Ouro Preto (LSFA07) and Salvador (LSFA08), always as a satellite event to the Brazilian Symposium on Formal Methods (SBMF). In 2009 (LSFA09), it was held as a satellite event of RDP 2009 in Brasília, and subsequently, it was a satellite event of ICTAC in Natal (LSFA10). Since its sixth edition, it has been held alone in Belo Horizonte (LSFA11), Rio de Janeiro and Niteroi (LSFA12) and São Paulo (LSFA13). In the last years, LSFA was held in Brasília (LSFA14) and then in Natal (LSFA15) as part of NAT@Logic 2015. The eleventh edition, (LSFA16), was held as a satellite event of FSCD 2016 in Porto, the twelfth edition, (LSFA17), in Brasília, as a satellite of the collocated conferences Tableaux+FroCoS+ITP, the thirteenth edition, (LSFA18), was held alone in Fortaleza, the fourteenth edition, (LSFA19), as a satellite of CADE 2019 in Natal. The fifteenth edition (LSFA20) took place in Bahia with the First Brazilian Workshop on Logic WBL.

LSFA aims to bring researchers and students interested in theoretical and practical aspects of logical and semantic frameworks and their applications. The covered topics include proof theory, type theory and rewriting theory, specification and deduction languages, and formal semantics of languages and systems. For LSFA 2021, seven regular papers were accepted for presentation out of twelve complete submissions. At least three reviewers reviewed each submission, and an electronic Program Committee meeting was held using Voronkov's EasyChair system. The reviews were written by the PC members and one additional reviewer. After the meeting, revised versions of the papers were reviewed, from which six regular papers were finally included in this volume. Also, this volume includes a revised technical contribution related to the invited talk given by Alejandro Díaz-Caro.

The invited talks were given by:

We are most grateful for the work and support of the invited speakers.

We want to thank the PC members and the additional reviewers for doing such a great job writing high-quality reviews in time and participating in the electronic PC discussion. In addition to the PC members, the authors and the invited speakers, many people helped make LSFA 2021 a success. In particular, we would like to thank the LSFA 2021 Organisers, Daniele Nantes Sobrinho and Cristian F. Sottile, the FSCD 2021 Local Organisers, Alejandro Díaz-Caro and Carlos López Pombo; and the FSCD SC Workshop Chair, Jamie Vicary. All they worked hard and were highly instrumental in guaranteeing this success.

Mauricio Ayala-Rincón Eduardo Bonelli
Brasília DF Hoboken NJ
31st December 2021

LSFA 2021 Chairs

LSFA 2021 Program Committee Members and Additional Reviewer

LSFA Steering Committee