# 12th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017)

23-24 September 2017 - Universidade de Brasília, Brazil

Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provide foundations for formal specification of systems and programming languages, supporting tool development and reasoning.

LSFA 2017 aims to be a forum for presenting and discussing work in progress, and therefore to provide feedback to authors on their preliminary research. The proceedings are produced after the meeting, so that authors can incorporate this feedback in the published papers.

LSFA 2017 will be a satellite event of the 26th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux 2017), the 11th International Symposium on Frontiers of Combining Systems (FroCoS 2017) and the 8th International Conference on Interactive Theorem Proving (ITP 2017) to be held in Brasília, Brazil, between 25 and 29 September 2017.

Previous editions took place in Porto (2016), Natal (2015), Brasília (2014), São Paulo (2013), Rio de Janeiro (2012), Belo Horizonte (2011), Natal (2010), Brasília (2009), Salvador (2008), Ouro Preto (2007) and Natal (2006).

## Topics of Interest

Topics of interest to this forum include, but are not limited to:

- Automated deduction
- Applications of logical and/or semantic frameworks
- Computational and logical properties of semantic frameworks
- Formal semantics of languages and systems
- Implementation of logical and/or semantic frameworks
- Lambda and combinatory calculi
- Logical aspects of computational complexity
- Logical frameworks
- Process calculi
- Proof theory
- Semantic frameworks
- Specification languages and meta-languages
- Type theory

## Submission

Contributions should be written in English and submitted in the form of full papers with a maximum of 16 pages including references or short papers with a maximum of 6 pages including references. Additional technical material can be provided in a clearly marked appendix which will be read by reviewers at their discretion. Contributions must also be unpublished and not submitted simultaneously for publication elsewhere. The papers should be prepared in LaTeX using the **generic ENTCS package** (http://www.entcs.org/prelim.html). The submission should be in the form of a PDF file uploaded to Easychair:

https://easychair.org/conferences/?conf=lsfa2017

The workshop pre-proceedings, containing the reviewed extended abstracts, will be handed-out at workshop registration. After the workshop the authors of both full and short papers will be invited to submit full versions of their works for the post-proceedings to be published in ENTCS. At least one of the authors should register for the conference. Presentations should be in English.

## Important dates

- Abstract:
**PLEASE SUBMIT AN ABSTRACT BY 23 JUNE 2017** - Submission:
~~21 June 2017~~**DEADLINE EXTENDED TO: 28 JUNE 2017** - Notification:
~~21 July 2017~~ - Final pre-proceedings version due:
~~11 August 2017~~ - LSFA 2017: 23-24 September 2017

## Invited speakers

- Beniamino Accattoli - INRIA
**(In)Efficiency and Reasonable Cost Models**This talk is about time cost models for the lambda-calculus. To allow the definition of basic complexity classes such as P or EXP directly in the lambda-calculus, a cost models has to be reasonable, that is, polynomially related to the one of Turing machines. For the lambda-calculus the existence of an evaluation strategy whose number of steps is a reasonable cost model has been a long-standing open problem. Positive answers to special cases were known since 1995, but a solution for the general case has been provided only in 2014. The problem is peculiar because some of its aspects are somewhat counter-intuitive. The talk is devoted to explain the subtleties of this fundamental topic, and to survey the results obtained so far. The key point that is often misunderstood, and on which we will focus, is that being efficient and being reasonable are two unrelated properties of evaluation strategies.

- Hélène Kirchner - INRIA
**Strategic Port Graph Rewriting in Porgy, an Interactive Modelling Framework**The Porgy framework is based on strategic port graph rewriting to design executable specifications of complex systems. A system is represented by an initial graph and a collection of graph rewrite rules, together with a user-defined strategy to control the application of rules. The traditional operators found in strategy languages for term rewriting have been adapted to deal with the more general setting of graph rewriting, and some new constructs have been included in the strategy language to deal with graph traversal and management of rewriting positions. The talk will describe and illustrate the main concepts underlying the Porgy framework through examples from biological systems and social networks.

- Renate Schmidt - University of Manchester
**Automated Forgetting and Uniform Interpolation for Description Logics**Forgetting eliminates symbols from a knowledge base so that consequences over the remaining symbols in the signature are preserved. In logic the problem has been studied as the uniform interpolation problem, a notion related to the Craig interpolation problem, but stronger. In computer science the importance of forgetting can be found in the knowledge representation literature, specification refinement literature and the area of description logic-based ontology engineering. In ontology-based information processing, forgetting allows users to focus on specific parts of ontologies in order to create decompositions and restricted views for in depth analysis or sharing with other users. Forgetting is also useful for information hiding, explanation generation. semantic difference computation and ontology debugging. Because forgetting is an inherently difficult problem - it is much harder than standard reasoning (satisfiability testing) - and very few logics are known to be complete for forgetting (or have the uniform interpolation property), there has been insufficient research on the topic and few forgetting tools are available.

In recent work we have developed practical methods for computing uniform interpolants for ontologies defined in expressive OWL language dialects. These can forget both concept and role symbols and can handle ontologies specified in description logics from ALC to extensions of ALC with role inclusions, transitive roles role inverse and number restrictions and ABox statements. Another strand of our research investigates and develops practical methods for semantic forgetting, which is stronger than uniform interpolation. These methods can perform concept and role forgetting for expressive description logics with number restrictions, nominals, role inclusions, role inverse, role conjunction and the top role. Experiments on a large number of ontologies from real-world applications have shown both methods are practical.

This is joint work with Patrick Koopmann and Yizheng Zhao.

## Committees

### Program Committee

- Sandra Alves, University of Porto -
**co-chair** - Renata Wassermann, University of São Paulo -
**co-chair** - Flávio L. C. de Moura, Universidade de Brasília -
**local organiser** - Carlos Areces, Universidad Nacional de Córdoba
- Mauricio Ayala-Rincon, Universidade de Brasilia
- Veronica Becher, Universidad de Buenos Aires
- Mario Benevides, Universidade Federal do Rio de Janeiro UFRJ
- Walter Carnielli, Centre for Logic, Epistemology and the History of Science – CLE
- Carlos Castro, UT Federico Santa Maria
- Kaustuv Chaudhuri, INRIA
- Marcelo Coniglio, UNICAMP
- Valeria De Paiva, University of Birmingham
- Santiago Escobar, Universitat Politècnica de València
- Amy Felty, University of Ottawa
- Maribel Fernández, King's College London
- Marcelo Finger, Universidade de Sao Paulo
- Ichiro Hasuo, University of Tokyo
- Edward Hermann Haeusler, PUC-Rio
- Delia Kesner, Université Paris-Diderot
- Bjoern Lellmann, TU Vienna
- Vivek Nigam, Universidade Federal da Paraíba
- Jorge A. Pérez, University of Groningen and CWI, Amsterdam
- Petrucio Viana, Universidade Federal Fluminense
- Elaine Pimentel, UFRN
- Giselle Reis, CMU-Qatar
- Camilo Rocha, Pontificia Universidad Javeriana Cali
- Simona Ronchi Della Rocca, Universita' di Torino
- Alvaro Tasistro, Universidad ORT Uruguay
- Christian Urban, King's College London

### Organizing Committee

- Flávio L. C. de Moura (Universidade de Brasília)
- Sandra Alves, University of Porto
- Renata Wassermann, University of São Paulo

## Registration

The registration page is now open. All prices are all given in Brazilian Reals. Regular fees include coffee breaks, lunchs, proceedings of the selected conferences/workshops, and social activities. Student fees include coffee breaks, lunchs, proceedings of the selected conferences/workshops, but do not include social activities (excursion/dinner).

- Early registration is until the
**4th August**. - Late registration until the 2nd September. After that, registration can be done only on the venue at the same prices of late registration, but only payment in cash can be taken.

## Accepted papers

- Arve Gengelbach and Tjark Weber.
**Model-Theoretic Conservative Extension for Definitional Theories** - Florian Rabe.
**The MMT Perspective on Conservativity** - Emmanuel Gunther, Miguel Pagano and Alejandro Gadea.
**Formalization of Universal Algebra in Agda** - Mohamed Yousri Mahmoud and Amy Felty.
**Formal Meta-level Analysis Framework for Quantum Programming Languages** - Bruno Xavier, Carlos Olarte, Giselle Reis and Vivek Nigam.
**Mechanizing Linear Logic in Coq** - Alexandre Madeira, Renato Neves, Manuel A. Martins and Luis Barbosa.
**Hierarchical hybrid logic** - Robin Kaarsgaard.
**Inversion, Fixed Points, and the Art of Dual Wielding** - Mario Benevides, Alexandre Madeira and Manuel A. Martins.
**A family of graded epistemic logics** - Stefano Del Vecchio and Virgile Mogbil.
**An interpretation of CCS into Ludics** - Andrés Felipe Barco Santa.
**Espistemic and Spatial Modeling Under a Constraint-Based Interpreter** - Guillermo Calderón.
**Formalizing Constructive Projective Geometry in Agda** - Polina Vinogradova, Amy Felty and Philip Scott.
**Formalizing Abstract Computability: Turing Categories in Coq** - Alejandro Díaz-Caro and Guido Martínez.
**Confluence in Probabilistic Rewriting** - Ernesto Copello, Nora Szasz and Alvaro Tasistro.
**Machine-checked proof of the Church-Rosser theorem for Lambda-Calculus using the Barendregt Variable Convention in Constructive Type Theory** - Jefferson Santos, Bruno Lopes and Edward Hermann Haeusler.
**Counter-Model Generation from Failed Proof Searches in Propositional Minimal Implicational Logic** - Thiago N. Silva and Umberto Rivieccio.
**Algebraic semantics for Nelson’s logic S** - Mauricio Ayala-Rincon, Besik Dundua, Temur Kutsia and Mircea Marin.
**Rewriting Logic from a $ρ$Log Point of View** - Valeria de Paiva and Harley Eades III.
**Dialectica Categories for the Lambek Calculus**