ABSTRACT. Logic has been acknowledged as potentially important to software engineering for as long as the latter field has existed. Yet, in practice, most software today is built without explicit reliance on logic, and often by people who do not think of themselves as having any knowledge of formal logic. I will claim that this is unlikely to change. Does that mean logic is not useful to software engineering? Of course not: but it means its role may be implicit more than explicit, or concealed in language and tool design. I will discuss some of the ways I have seen logic turn up in model-driven software development, in particular, and try to point out some interesting challenges for the future.

ABSTRACT. Translating formulas of Linear Temporal Logic (LTL) over finite traces, or LTLf, to symbolic Deterministic Finite Automata (DFA) plays an important role not only in LTLf synthesis, but also in synthesis for Safety LTL formulas. The translation is enabled by using MONA, a sophisticated tool for symbolic DFA construction from logic specifications. Recent works used a first-order encoding of LTLf formulas to translate LTLf to First Order Logic (FOL), which is then fed to MONA to construct the symbolic DFA. This encoding was shown to perform well, but other encodings have not been studied. Specifically, the natural question of whether second-order (MSO) encoding, which has significantly simpler quantificational structure, can outperform first-order (FOL) encoding remained open.

In this paper we meet this challenge and study MSO encoding for LTLf formulas. We introduce a specific MSO encoding, and show that this encoding and its simplicity indeed allow more potential than FOL for optimization, thus benefiting symbolic DFA construction. We then show by empirical evaluations that, surprisingly, the FOL encoding outperforms in practice the MSO encodings. We analyze the results and explain how to improve MONA in order to allow the MSO encoding to outperform the FOL encoding.

ABSTRACT. We propose a new type system for deadlock-free session-typed π-calculus, a core concurrent programming language, by integrating for the first time, two separate lines of work. The first is the propositions-as-types approach by Caires and Pfenning, which provides a linear logic foundation for session types and guarantees deadlock-freedom. The second is Kobayashi’s approach in which types are annotated with priorities for detecting cyclic dependencies between communication operations. The outcome is a new and more expressive variant of classical linear logic with a proof assignment that gives a session type system with Kobayashi-style priorities.

ABSTRACT. Brouwer developed the notion of mental constructions based on his view of mathematical truth as experienced truth. These constructions extend the traditional practice of constructive mathematics, and we believe they have the potential to provide a broader and deeper foundation for various constructive theories.We here illustrate mental constructions in two well studied theories – computability theory and plane geometry – and discuss the resulting extended mathematical structures. Further, we demonstrate how these notions can be embedded in an implemented formal framework, namely the constructive type theory of the Nuprl proof assistant. Additionally, we point out several similarities in both the theory and implementation of the extended structures.

ABSTRACT. The thesis that any mathematical proof can be formalized was advocated by (among others) Hilbert and Gentzen around a century ago. The Hilbert-Gentzen thesis says: “Every real proof can be represented by a formal proof.” This article will go through several possible interpretations of this thesis, to be able to understand and discuss it fairly. To be able to fully understand the reasoning that separates the different interpretations, there will be a discussion on the different arguments for why formalisation has the status it currently has within mathematics. The H-G thesis has held a firm place in the foundations and philosophy of mathematics since these thoughts were first expressed a century ago. However the recent “informal proofs debate” gives us several arguments against the thesis, arguing that it is false and that it should be rejected. This talk will (1) define the thesis with help from the context in which it was introduced, (2) give the main arguments for accepting it, (3) give the main arguments for refuting it, as stated by M. Marfori, C. Cellucci, K. gödel, and F. Tanswell, and then (4) evaluate the strength and scope of the arguments and counter arguments. This talk will be a summarization and discussion on the current status of the Hilbert-Gentzen thesis, and the conclusion will be that the thesis overestimates the value of formalisation and that the thesis should be rejected.

ABSTRACT. In this work, we explore proof theoretical connections between sequent, nested and labelled calculi. In particular, we show a semantical characterisation of intuitionistic, normal and non-normal modal logics for all these systems, via a case-by-case translation between labelled nested to labelled sequent systems.

ABSTRACT. We present a labelled deduction for intuitionistic modal logic that comes with two relation symbols, one for the accessible world relation associated with the Kripke semantics for modal logics, and one for the preorder relation associated with the Kripke semantics for intuitionistic logic. Thus, our labelled system is in close correspondence to the birelational Kripke models.

ABSTRACT. We introduce a new inference problem for topological logics, the unifiability problem. Our main result is that, within the context of the mereotopology of all regular closed polygons of the real plane, unifiable formulas always have finite complete sets of unifiers.

ABSTRACT. Mechanizing formal systems, given via axioms and inference rules, together with proofs about them plays an important role in establishing trust in formal developments. Over the past decade, the POPLMark challenge popularized the use of proof assistants in mechanizing the metatheory of programming languages. Focusing on the the meta-theory of System F with subtyping, it allowed the programming languages community to survey existing techniques to represent and reason about syntactic structures with binders and promote the use of proof assistants. Today, mechanizing proofs is a stable fixture in the daily life of programming languages researchers.

As a follow-up to the POPLMark Challenge, we propose a new collection of benchmarks that use proofs by logical relations. Such proofs are now used to attack problems in the theory of complex languages models, with applications to issues in equivalence of programs, compiler correctness, representation independence and even more intensional properties such as non-interference, differential privacy and secure multi-language inter-operability. Yet, they remain challenging to mechanize. In this talk, we focus on one particular challenge problem, namely strong normalization of a simply-typed lambda-calculus with a proof by Kripke-style logical relations. We will advocate a modern view of this well-understood problem by formulating our logical relation on well-typed terms. Using this case study, we share some of the lessons learned tackling this challenge problem in Beluga, a proof environment that supports higher-order abstract syntax encodings, first-class context and first-class substitutions. We also discuss and highlight similarities, strategies, and limitations in other proof assistants when tackling this challenge problem. We hope others will be motivated to submit solutions! The goal of this talk is to engage the community in discussions on what support in proof environments is needed to truly bring mechanized metatheory to the masses.

This is joint work with Andreas Abel (Chalmers), Aliya Hameer (McGill), Alberto Momigliano (Univ. of Milan), Steven Schäfer (Univ. Saarbrücken), Kathrin Stark (Univ. Saarbrücken)

ABSTRACT. Proving properties about proof systems is a necessary task to make sure that they are sound and satisfy basic criteria for the application being considered. Nevertheless, it is a tedious and error-prone task. In this talk, I will present on-going work on the development of a trustworthy system that helps with the verification of proof calculi's properties. This system allows for a natural specification of sequent-style calculi and visualization of rules in LaTeX. The user is also able to construct simple proof trees. Moreover, it can be used to check identity expansion, cut-elimination and permutation lemmas with the click of a button. Our goal is to free researchers from having to write down big and repetitive proofs, and move towards the use of mechanized proofs when meta-theory of proof systems is concerned.

ABSTRACT. Transitive closure logic is obtained by a modest addition to first-order logic that affords enormous expressive power. Most importantly, it provides a uniform way of capturing finitary inductive definitions. Thus, particular induction principles do not need to be added to the logic; instead, all induction schemes are available within a single, unified language. We here present a non-well-founded proof system for transitive closure logic which is complete for the standard semantics. This system captures implicit induction, and its soundness is underpinned by the principle of infinite descent. We also consider its subsystem of cyclic proofs.

ABSTRACT. In recent work we have proposed a calculus for the multimodal logic K, where clauses are labelled by the modal level in which they occur. The calculus has been implemented and the evaluation shows that the prover performs well if the propositional symbols are uniformly distributed over the modal levels. However, by construction, the set of propositional clauses is always satisfiable. We are investigating the combination of SAT provers with our prover, in order to extract relevant information that could help reducing the time currently used during saturation.

ABSTRACT. Intuitionistic logics have shown to constitute the foundations for many practical applications. For example, they serve as basis for state-of-the art proof assistents like Coq. Nevertheless, they have also been controversially discussed. David Hilbert wrote that: "Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists."[4] Indeed, this property of intuitionistic logic gives rise to plenty of new challenges. When trying to embed intuitionistic logics in higher-order logic, monotonicity has to be minded. Furthermore, it is desirable to prove a set of frame conditions equivalent to the axioms used to build different intuitionistic logics. This talk will give a short overview on the challenges occurring due to the absence of the principle of excluded middle and discuss possible solutions.

ABSTRACT. Modelling in psychometrics has become increasingly reliant on computer software; at the same time, many offline decisions that a researcher makes remain unrecorded and perhaps, unreconciled to anything more than the researcher’s intuition or best guess. The aim of this paper is to set out a logic that accounts for and guides accounting for decision procedures in psychometric research practices. Such a logic is informed by the integration of three systematic viewpoints under a view of constraints-based practice: i) bounded rationality (Gigerenzer & Goldstein, 1996); ii) axiomatic measurement theory with specific focus on handling measurement uncertainty (Suppes, 2002, 2006, 2016); and iii) a constructive approach to mathematical set theory (Ferreiros, 2016). The integration of these three viewpoints under an overall perspective that is characterised by inference from the best systematisation (Rescher, 2016) is reviewed, and compared to current researcher practices, with particular reference to the problems for psychometric and biometric sciences that are revealed in the Reproducibility Project (Open Science Collaboration, 2012) outcomes. Our conclusion for the overall system is that the constraints characterised by constructive mathematics offer unique tools to researcher communities in accounting for their decision procedures, and a proposal for a software tool that handles the decision protocol is presented. In characterising the decision procedures, we also explore the way that rough set theory (Pawlak, 1998) is integrated into decision procedures to provide insight into database fields or variables that hold some import but may otherwise remain hidden in research outcome reporting.