Check the Title and Abstract
of our Invited Talks!
Gilles Barthe (IMDEA Software Institute)
Kaustuv Chaudhuri (INRIA/École Polytechnique)
Luis Caires (Universidade Nova de Lisboa)
João Marques Silva (Universidade de Lisboa)
lsfa2016[at]mat.unb.br
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.
The objective of this workshop is to bring together theoreticians and
practitioners to promote new techniques and results, and to
facilitate feedback on the implementation and application of such techniques and
results in practice.
LSFA 2016 also 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 2016 will take place on June 25-26 2016 as satellite of Formal Structures for Computation and Deduction (FSCD'16) in
Porto. Previous editions took place in 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).
More information about LSFA can be found by clicking here.
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 ENTCS style. The submission should be in the form of a PDF file uploaded to Easychair:
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. A common theme in program verification is to relate two programs, for instance to show that they are equivalent, or that one refines the other. Such relationships can be formally established using relational program logics, which are tailored to reason about relations between two programs, or product constructions which allow to build from two programs a product program that emulates the behavior of both input programs. Similarly, product programs and relational program logics can be used to reason about 2-safety properties, an important class of properties that reason about two executions of the same program, and includes non-interference and continuity, and other notions such as truthfulness (a concept from game theory) and differential privacy.
In this talk, I shall present an overview of relational program logics and product programs and explore their relationship, both in the context of imperative and higher-order languages.
Abstract. Logics and type systems are closely related: given a sufficiently general type system, many logics can be defined in terms of typed signatures. This is the design of the Edinburgh Logical Framework (LF) [4], to take a prototypical example, where the dependently typed λ-calculus is taken as a uniform representation of the syntax, rules, and proofs of candidate object logics. The opposite perspective is comparatively less common: in a suitably general logic, a wide variety of type systems can be defined in terms of adequate relational encodings [2].
This talk demonstrates this latter perspective by showing how to capture:
in an extension of the two-level logic approach [5,3] to specification and reasoning, implemented as a fork of the Abella theorem prover [1]. Each type system is represented by:
Abstract While type systems for more traditional programming abstractions have been rooted on pure logical principles, im the sense of Curry-Howard correspondences, the connections between session-based concurrent programming languages and their logically motivated type disciplines only started to be better understood recently. In this talk, we review some of our recent work on the theme, and discuss extensions to non-deterministic interaction.
Abstract.The success of propositional satisfiability (SAT) solvers is underscored by their ubiquitous use in practical applications. Whereas many practical applications can be cast as decision problems, for which a single query to a SAT oracle suffices, for many other applications, SAT oracles are called multiple times. For example, this is the case when solving decision problems with abstraction refinement, e.g. bit-vector formulas in SMT. This is also the case when solving decision problems in higher levels of the polynomial hierarchy, e.g. QBF. Moreover, many computational problems are naturally formulated as function (or search) problems, and can be solved with a number of queries to a SAT oracle. This talk overviews problem- solving based on multiple queries to a SAT oracle, focusing on approaches for solving function problems.
The talk presents a number of function problems defined on Boolean formulas and shows how most of these problems can be reduced to the problem of computing a minimal set subject to a monotone predicate. The talk also surveys a number of algorithms for the MSMP problem, highlighting the worst-case number of SAT oracle queries. Finally, the talk overviews ongoing research in the area of problem solving with SAT oracles.
