| CARVIEW |
COVID19 Update
The 17th International Workshop on Logical and Semantic Frameworks, with Applications (LSFA) will be held in Belo Horizonte on Sep 23 and Sep 24, 2022.
MoreAbout LSFA22
The 17th International Workshop on Logical and Semantic Frameworks, with Applications (LSFA) will be held in Belo Horizonte, MG, Brazil on September 23 and 24, 2022.
Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provide foundations for the formal specification of systems and programming languages, supporting tool development and reasoning.
Previous editions of LSFA took place in Buenos Aires (2021, online, as a satellite of FSCD 2021), Bahia (2020, online, collocated with the First Brazilian Workshop on Logic WBL), Natal (2019), Fortaleza (2018), Brasília (2017, collocated with Tableaux+FroCoS+ITP), 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). See https://lsfa.cic.unb.br for more information.
NOTE ABOUT COVID-19
The Program Committee and the local organization of LSFA are following closely the information regarding the spread and incidence of the coronavirus in Brazil, as given by local authorities and the World Health Organization. We are currently planning an hybrid event, but the conference will be foremost designed for in-person participation: for the most fruitful participation we strongly encourage people to participate in person.
Call for Papers
17th Workshop on Logical and Semantic Frameworks, with Applications
23-24 September 2022, Belo Horizonte, Brazil.
Logical and semantic frameworks are formal languages used to represent logics, languages and systems. These frameworks provide foundations for the formal specification of systems and computational languages, supporting tool development and reasoning.
Previous editions of LSFA took place in Natal (2019), Fortaleza (2018), Brasília (2017), 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).
See https://lsfa.cic.unb.br for more information.
Topics of interest include, but are not limited to:
- Automated deduction
- Applications of logical and semantic frameworks
- Computational and logical properties of semantic frameworks
- Formal semantics of languages and systems
- Implementation of logical and 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 and Publication
Contributions should be written in English and submitted in full paper (with a maximum of 16 pages excluding references) or short papers (with a maximum of 6 pages excluding references). They must be unpublished and not submitted simultaneously for publication elsewhere. The papers should be prepared in LaTeX using the EPTCS style. The submission should be in the form of a PDF file uploaded to Easychair
The pre-proceedings, containing the reviewed papers, will be available on the web page. After the meeting, the authors will be invited to submit full versions of their works for the post-proceedings publication. At least one of the authors of each submission must register for the conference. Presentations should be in English. According to the submissions' quality, the chairs will promote the further publication of journal revised versions of the papers. Previous LSFA Special Issues have been published in journals such as The Logical J. of the IGPL, Theoretical Computer Science and Mathematical Structures in Computer Sciences (see the LSFA page https://lsfa.cic.unb.br).
Important Dates
- Abstract deadline: Monday 16 May (Extended, Anywhere on Earth)
- Submission deadline: Monday 23 May (Extended, AoE)
- Notification to authors: Saturday 9 July (AoE)
- Preliminary proceedings version due: Thursday 1 September (AoE)
- LSFA 2022: Friday-Saturday 23-24 September
- Submission for final EPTCS proceedings: Monday 17 October (AoE)
- Final version: Monday 21 November (AoE)
Program
All time slots are mentioned in Belo Horizonte / BRT / Brasília Time (UTC-3)
THE PROGRAM IS SUBJECT TO CHANGE
Detailed Program:
The detailed program for each day can be viewed by clicking in the specific day on the resumed program above. Alternatively, the detailed program can be viewed in the link below.
Detailed Schedule (subject to change!)LSFA Proceedings:
The LSFA 2022 Pre-Proceedings are available for download here.
September 23
-
08:55 - 09:00 Welcome to LSFA
-
09:00 - 09:30 Nominal Sets in Agda - A Fresh and Immature Mechanization
Miguel Pagano and José Solsona -
09:30 - 10:00 A Formal Proof of the Strong Normalization Theorem for System T in Agda
Sebastián Urciuoli -
10:00 - 10:30 ReLo: A Dynamic Logic to Reason about Reo Circuits
Erick Grilo and Bruno Lopes -
10:30 - 11:00 Coffee Break
-
11:00 - 11:30 Analyzing Innermost Runtime Complexity Through Tuple Interpretations
Liye Guo and Deivid Vale -
11:30 - 12:00 Towards a Proof in Lean about the Horizontal Compression of Dag-Like Derivations in Minimal Purely Implicational Logic
Robinson Callou, Jefferson Santos and Edward Haeusler -
12:00 - 14:00 Lunch Break
-
14:00 - 15:00 Invited Talk: Cláudia Nalon
-
15:00 - 15:30 Coffee Break
-
15:30 - 17:30 Tutorial: SMT, Haniel Barbosa
-
Evening Dinner
September 24
-
09:30 - 10:00 Extending the Quantitative Pattern-Matching Paradigm
Sandra Alves, Delia Kesner and Miguel Ramos -
10:00 - 10:30 Tool Support for Interval Specifications in Differential Dynamic Logic
Jaime Santos, Daniel Figueiredo and Alexandre Madeira -
10:30 - 11:00 Coffee Break
-
11:00 - 11:30 Equational Theorem Proving for Clauses over Strings
Dohan Kim -
11:30 - 12:00 Paraconsistent Transition Systems
Ana Cruz, Alexandre Madeira and Luís Soares Barbosa -
12:00 - 14:00 Lunch Break
-
14:00 - 15:00 Invited Talk: Ciro Russo
-
15:15 - 17:30 Logic BarWe meet at some nice place, have a drink, and informally discuss logic topics.
Topics will be collected during LSFA.
September 23
-
08:55 - 09:00 Welcome to LSFA
-
09:00 - 09:30 Nominal Sets in Agda - A Fresh and Immature Mechanization
Miguel Pagano and José Solsona -
09:30 - 10:00 A Formal Proof of the Strong Normalization Theorem for System T in Agda
Sebastián Urciuoli -
10:00 - 10:30 ReLo: A Dynamic Logic to Reason about Reo Circuits
Erick Grilo and Bruno Lopes -
10:30 - 11:00 Coffee Break
-
11:00 - 11:30 Analyzing Innermost Runtime Complexity Through Tuple Interpretations
Liye Guo and Deivid Vale -
11:30 - 12:00 Towards a Proof in Lean about the Horizontal Compression of Dag-Like Derivations in Minimal Purely Implicational Logic
Robinson Callou, Jefferson Santos and Edward Haeusler -
12:00 - 14:00 Lunch Break
-
14:00 - 15:00 Invited Talk: Cláudia Nalon
-
15:00 - 15:30 Coffee Break
-
15:30 - 17:30 Tutorial: SMT, Haniel Barbosa
-
Evening Dinner
September 24
-
09:30 - 10:00 Extending the Quantitative Pattern-Matching Paradigm
Sandra Alves, Delia Kesner and Miguel Ramos -
10:00 - 10:30 Tool Support for Interval Specifications in Differential Dynamic Logic
Jaime Santos, Daniel Figueiredo and Alexandre Madeira -
10:30 - 11:00 Coffee Break
-
11:00 - 11:30 Equational Theorem Proving for Clauses over Strings
Dohan Kim -
11:30 - 12:00 Paraconsistent Transition Systems
Ana Cruz, Alexandre Madeira and Luís Soares Barbosa -
12:00 - 14:00 Lunch Break
-
14:00 - 15:00 Invited Talk: Ciro Russo
-
15:00 - 15:15 Business Meeting
-
15:15 - 17:30 Logic BarWe meet at some nice place, have a drink, and informally discuss logic topics.
Topics will be collected during LSFA.
Invited Talks
Ciro Russo
Federal University of Bahia, BrazilThe category of propositional deductive systems and their generalized models
Abstract:
Quantales and their modules provide an efficient framework for representing deductive systems [1], within which it is possible to deal with several important issues, e.g.: interpretation and equivalence, language expansion, combination of different logics (even with the preservation of a possible common fragment).
In this framework, a propositional language is canonically associated to a quantale, and any deductive system on such a language is identified with its own lattice of theories which, on its turn, is a left module over the given quantale.
It was proved in [1] that a system is interpretable (resp.: conservatively interpretable, equivalent) in another one with the same underlying language if and only if there exists a homomorphism (resp.: embedding, isomorphism) between the two respective modules of theories. Such a result has been extended to systems with different languages by introducing language translations and characterizing them among the quantale morphisms [2].
In a more recent paper [3], various other algebraic and categorical properties of quantales and their modules have been applied in order to manage language expansion, fragments and, above all, combination of different logics in a new system encompassing them.
We shall present an overview of the above results and then we will introduce a category in which deductive systems and their generalized matrix semantics (or generalized models) are a subclass of the object class, semantic and syntactic interpretations are morphisms and, moreover, all of the phenomena described above are just instances of general categorical concepts.
[1] Galatos, N., and Tsinakis, C.; Equivalence of consequence relations: an order-theoretic and categorical perspective. Journal of Symbolic Logic 74/3 (2009), 780-810.
[2] Russo, C.; An order-theoretic analysis of interpretations among propositional deductive systems. Annals of Pure and Applied Logic 164 (2) (2013), 112-130.
[3] Russo, C.; Coproduct and Amalgamation of Deductive Systems by Means of Ordered Algebras. Log. Univers. 16 (2022), 355–380.
Claudia Nalon
University of Brasília, BrazilWebsite
https://nalon.org/From Global to Local: Complexity Preserving Reductions for the Modal Cube into K
Abstract: Modal logics are applied to represent and reason about a large variety of complex problems: from the formalisation of Mathematics and philosophical problems to applications in Computer Science and Engineering. Such applications might require specific extensions of modal logics that better represent constraints for a particular given domain, which can be achieved by adding to K (normality) the axioms B (symmetry), D (seriality), T (reflexivity), 4 (transitivity), and 5 (Euclideaness). The logics arising from these axioms and their combinations comprise what is known as the modal cube. Given the wide range of applications, the availability of automatic tools for reasoning about problems represented in these logics is highly desirable. But that is not the case. Although both model and proof theory for the considered logics are well developed and understood, there is a lack of automatic modal reasoners. Therefore, automated reasoning for modal logics often exploits the fact that their languages can be translated into stronger logics, as first-order logic, for which there are readily available, reliable provers. This is however problematic, as the translation might not retain complexity and might not even lead to a decision procedure. In this talk, we will argue in the other direction: many modal logics can also be efficiently translated into weaker logics whilst preserving decidability and complexity results. We provide translations directly into a clausal normal form for K which is suitable for automatic reasoning using modal resolution. Experimental evaluation with our own prover, KSP, shows that we can achieve good performance for all the logics in the modal cube. Other automated tools for local reasoning in K, whose availability is higher than those for specific normal modal logics, could also benefit from the techniques utilised in our translation.
Registration
Registration for LSFA 2022 is free, but needs though the
Program Committee
Venue & Location
The conference will take place at the Pampulha campus of Universidade Federal de Minas Gerais (UFMG) in Belo Horizonte, the capital of the Brazilian state of Minas Gerais. With over 6M people, Belo Horizonte's metropolitan area is the third largest in Brazil.
Venue: LFSFA 2022 will be held in the ICEx building at UFMG, room 2077.
Travel information:
The closest airport is Confins
International (CNF). There is a dedicated coach service between
the airport and the Pampulha region (~40min), as
well as the city center (~1h). It costs 37 BRL for
the higher quality bus, 17 BRL for the conventional
one.
A taxi ride from CNF to city center will cost around
120 BRL. An uber ride should be around 90 BRL.
Support
South-american student authors are elegible to financial aid for travel costs to LSFA 2022. Please get in contact via e-mail.