LSFA 2019
14th International Workshop on Logical and Semantic Frameworks, with Applications
Natal, Brazil
Aug 25-26, 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
- Mauricio Ayala-Rincon, Maribel Fernandez, Daniele Nantes-Sobrinho and Deivid Vale. On Solving Nominal Disunification Constraints
- Leandro Gomes, Alexandre Madeira and Luis Barbosa. Introducing synchrony in fuzzy automata
- Manisha Jain, Alexandre Madeira and Manuel A. Martins. A Fuzzy Modal Logic for Fuzzy transition systems
- Uwe Wolter, Alfio Martini and Edward Haeusler. Indexed and Fibred Structures for Hoare Logic [slides]
- Vitor Machado and Mario Benevides. Populational Announcement Logic (PPAL) [slides]
- Miguel Campercholi, Mauricio Tellechea and Pablo Ventura. Deciding Open Definability in Algebraic Structures
- 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
Venue
Photo album
Please follow this link.