LSFA 2019

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 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 http://lsfa.cic.unb.br for more information. The 2019 edition will take place at UFRN, in Natal, as a satellite event of CADE-27.

Submissions

The Call For Papers may be found here.

Topics of interest include, but are not limited to:

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

Contributions should be written in English, using the generic ENTCS package, and submitted in the form of full papers with a maximum of 13 pages, including references. The submission should be in form of a PDF file uploaded here.

Important Dates

• May 1, 2019 (Apr 19, 2019): Submission deadline
• June 5, 2019 (May 24, 2019): Notification to authors
• Jun 26, 2019 (Jun 21, 2019): Proceedings version due
• Aug 25-26, 2019: Workshop

Registration

Please visit this link.

Committees

Programme Committee

• Amy Felty, University of Ottawa (chair)
• João Marcos, UFRN (chair)
• Beniamino Accattoli, INRIA (Saclay)
• Sandra Alves, University of Porto
• Mario Benevides, UFRJ
• Ana Bove, Chalmers
• Marco Cerami, UFBA
• Valeria de Paiva, Nuance Communications
• Maribel Fernandez, King's College London
• Francicleber Ferreira, UFC
• Erich Grädel, RWTH Aachen
• Edward Hermann Haeusler, PUC-Rio
• Oleg Kiselyov, Tohoku University
• Björn Lellmann, TU Wien
• Bruno Lopes, UFF
• Favio Miranda-Perea, UNAM
• Alberto Momigliano, University of Milano
• Daniele Nantes, UnB
• Pedro Quaresma, University of Coimbra
• Florian Rabe, LRI Paris
• Alexandre Rademaker, IBM-Brazil
• Umberto Rivieccio, UFRN
• Camilo Rocha, PUJ
• Matthieu Sozeau, IRIF
• Nora Szasz, Universidad ORT
• Ivan Varzinczak, Université d’Artois
• Daniel Ventura, UFG
• Anna Zamansky, University of Haifa

Organizing Committee

• Cláudia Nalon (UnB) and Carlos Olarte (UFRN).

Invited Speakers

• Pascal Fontaine, LORIA: Handling quantifiers in SMT (joint work with Haniel Barbosa and Andrew Reynolds) [slides]
• Achim Jung, University of Birmingham: Separating truth from falsity (joint work with Umberto Rivieccio) [slides]
• Vivek Nigam, Fortiss: Formal Security Verification of Industry 4.0 Applications (joint work with Carolyn Talcott) [slides]
• Elaine Pimentel, UFRN: An Ecumenical Notion of Entailment (joint work with Luiz Carlos Pereira & Valeria de Paiva) [slides]
• Giselle Reis, CMU-Qatar: Linear Logical Frameworks [slides]

Accepted Contributions

Full Papers

1. Mauricio Ayala-Rincon, Maribel Fernandez, Daniele Nantes-Sobrinho and Deivid Vale. On Solving Nominal Disunification Constraints
2. Leandro Gomes, Alexandre Madeira and Luis Barbosa. Introducing synchrony in fuzzy automata
3. Manisha Jain, Alexandre Madeira and Manuel A. Martins. A Fuzzy Modal Logic for Fuzzy transition systems
4. Uwe Wolter, Alfio Martini and Edward Haeusler. Indexed and Fibred Structures for Hoare Logic [slides]
5. Vitor Machado and Mario Benevides. Populational Announcement Logic (PPAL) [slides]
6. Miguel Campercholi, Mauricio Tellechea and Pablo Ventura. Deciding Open Definability in Algebraic Structures
7. Lourdes Del Carmen González Huesca, Favio E. Miranda-Perea and Pilar Selene Linares. Dual and Axiomatic systems for constructive S4, a formally verified equivalence [slides]

Short Papers

1. Bruno Olímpio, Jefferson Santos and Bruno Lopes. A framework to model check Blockchain using nuXmv [not presented]
2. Mario Benevides and Isaque Macalam Saab Lima. Dynamic Epistemic Logic with Assignments, Concurrency and Communication Actions [slides]

Venue

Photo album

Please follow this link.

Contact

lsfa2019-at-easychair.org

Sponsors