ABSTRACT. Welcome to the 9th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, LFMTP 2014. The LFMTP workshop series resulted from the amalgamation of the Logical Frameworks and Meta-languages (LFM) and the MEchanized Reasoning about Languages with variable bINding (MERLIN) workshop series. LFMTP 2014 is afflilated with two FLoC conferences: the joint meeting of the 23rd EACSL Annual Conference on Computer Science Logic and the 9th ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS), and the 7th International Joint Conference on Automated Reasoning (IJCAR). The full proceedings of LFMTP 2014 is available in the ACM Inernational Conference Proceedings Series at http://www.acm.org/publications/icp_series or http://dl.acm.org/icps.cfm?.

ABSTRACT. Indexing is generally viewed as an implementation artifact, indispensable to speed up the execution of logic programs and theorem provers, but with little intrinsically logical about it. We show that indexing can be given a justification in proof theory on the basis of focusing and linearity. We demonstrate this approach on predicate indexing for Horn clauses and certain formulations of hereditary Harrop formulas. We also show how to refine this approach to discriminate on function symbols as well.

ABSTRACT. We discuss the extension of the standard LF logical framework with operators for manipulating worlds, as found in hybrid logics or in the HLF framework. To overcome the restrictions of HLF, we present a more general approach to worlds in LF, where the structure of worlds can be described in an abstract way. We give a canonical presentation of the system and discuss the encoding of logical systems, beyond the limited scope of linear logic that formed the main goal of HLF.

ABSTRACT. The dependently-typed lambda calculus (LF) supports use of meta-level binding in reasoning about bindings and hypotheticals in programming languages. That is, lambda expressions in LF can be used to model binders and hypothetical judgments depending on fixed-size contexts. However, because LF does not have a concept of variable-arity functions, a hypothetical judgment depending on a variable-size context cannot be modeled as an LF function. This paper extends LF to support variable-arity functions. As a result, one can model hypothetical judgments with variable contexts directly in the extended LF. The extended LF is simpler and more powerful than previous work that uses complex meta-machinery to type the LF context. This is work in progress: we are still in the process of constructing a proof of correctness.

For more information: http://www.cs.uwm.edu/~boyland/papers/lf+variable.html

ABSTRACT. Session types and separation logic are two leading methodologies for software verification. Session types allow users to write protocols that concurrent programs must adhere to; a session type specifies the order in which messages have to be exchanged, and the types of the data those messages carry. By checking that programs follow compatible session types, we can reason about the ways processes interact, ultimately guaranteeing the absence of deadlocks and race conditions in sessions. Separation logic is an extension of Hoare logic that is typically used to prove full functional correctness of sequential stateful programs; using separation logic, we can write pre- and post-conditions for program statements that use mutable stores such as a heap and modularly verify that they satisfy these specifications. Separation logic is more expressive than session types when it comes to data: with it we can state properties such as "x is a number greater than five", whereas session types can only express that "x is a number". On the other hand, session types offer a powerful means of checking that the communications among concurrent programs do not interfere with each other or deadlock.

In this talk we describe a merger of session types and a higher-order separation logic by extending a Java-like programming language with send, receive, and fork primitives and adding session types to the Hoare logic. We combine the two methodologies to verify that a system of concurrent programs performs some communications to reach a common goal, which we define using separation logic assertions on their respective mutable stores. This allows us to verify programs like distributed sorting algorithms, where an agent can receive a list and later send a sorted version of that list. All other commands, such as loops, memory accesses and function calls are handled using separation logic in the usual way. We also maintain modular verification, as each agent is individually verified as if it were a sequential program.

This is a joint work with Morten Fangel Jensen and Fabrizio Montesi.

ABSTRACT. We focus on a common problem encountered in encoding and formally reasoning about a wide range of formal systems, namely, the representation of a typing environment. In particular, we apply the bookkeeping technique to a well-known case study (i.e., System F<:’s type language), proving in Coq an internal correspondence with a more standard representation of the typing environment as a list of pairs.

In order to keep the signature readable and concise, we make use of higher-order abstract syntax (HOAS), which allows us to deal smoothly with the representation of the universal binder of System F

ABSTRACT. It is well known that reasoning about substitution is a huge “distraction” that inevitably gets in the way of formalizing interesting properties of languages with variable bindings. Most formalizations have their own separate definitions of terms and substitution, and properties about it. However there is a great deal of uniformity in the way substitution works and the reasons why its properties hold. We expose this uniformity by defining terms, substitution and α-equality generically in Coq by parametrizing them over a Context Free Grammar annotated with Variable binding information (CFGV).

We also provide proofs of many properties about the above definitions (enough to formalize the PER semantics of Nuprl in Coq). Unlike many other tools which generate a custom definition of substitution for each input, all instantiations of our term model share the same substitution function. The proofs about this function have been accepted by Coq’s typechecker once and for all.

ABSTRACT. MMT implements a prototypical declarative language in a way that systematically abstracts from theoretical and practical aspects of individual logics. It tries to develop as many solutions as possible generically so that logic designers can focus on the essentials and inherit a large scale implementation at low cost.

For example, advanced generic features include module system, user interface, and change management. Here we focus on MMT's generic type reconstruction component and show how it can be customized to obtain implementations of various logics. As examples, we consider LF as well as its extensions with shallow polymorphism and rewriting.

ABSTRACT. The compilation of functional programs relies on transformations that simplify their structure while ostensibly preserving their meanings. We argue that the combination of the lambda Prolog language and the Abella interactive theorem-prover provide a natural framework for the verified implementation of such transformations. Underlying this argument is the fact that the transformations are syntax-directed and rule-based, with the important proviso that they pay attention to and also modify the binding structure of programs. The logic of higher-order hereditary Harrop formulas, the HoHH logic for short, is well-suited to formalizing such descriptions especially because of the support it provides for the higher-order representation of syntax. By virtue of the computational interpretation of the HoHH logic embodied in lambda Prolog, these formalizations become implementations of the corresponding transformations. The logic that underlies Abella embeds the HoHH logic and provides a complementary capability for reasoning flexibly and succinctly about the properties of specifications written in the HoHH logic. We will consider a typical functional program transformation and show how these twin capabilities can be exploited in its verified implementation; we will especially focus on demonstrating the benefits of a higher-order representation of syntax in both specification and reasoning. We will also discuss an extension to the logic underlying Abella for treating logical relations, a notion that is often needed in semantics preservation arguments.

The talk will draw on work done at various times with David Baelde, Alwen Tiu and Yuting Wang.

ABSTRACT. Hypothetical judgments go hand-in-hand with higher-order abstract syntax for meta-theoretic reasoning. Such judgments have two kinds of assumptions: those that are statically known from the specification, and the dynamic assumptions that result from building derivations out of the specification clauses. It is well known that these dynamic assumptions often have a simple regular structure of repetitions of blocks of assumptions that are introduced at the same time, with each block generally involving one or several variables and their properties that are added to the context in a single backchaining step. When this regular structure of a dynamic context is statically known, it is possible to automatically reflect on the structure to derive structural properties of its elements.

In this work, we present an extension of the Abella theorem prover, which is based on a simply typed intuitionistic reasoning logic supporting inductive and co-inductive definitions, where dynamic contexts are traditionally specified as inductive characterizations of lists of formulas. We add a new mechanism for defining particular kinds of regular context specifications, called schemas, and tacticals to derive theorems from these schemas as needed. Importantly, our extension leaves the core tactics and proof language of Abella unchanged, so it is manifestly certifying and fully compatible with existing developments. We show that these tacticals can eliminate many commonly encountered kinds of administrative lemmas that would otherwise have to be proven manually, which is a common source of complaints from Abella users.

ABSTRACT. The third round of the Kurt Gödel Research Prize Fellowships Program, under the title: Connecting Foundations and Technology, aims at supporting young scholars in early stages of their academic careers by offering highest fellowships in history of logic, kindly supported by the John Templeton Foundation. Young scholars being less or exactly 40 years old at the time of the commencement of the Vienna Summer of Logic (July 9, 2014) will be awarded one fellowship award in the amount of EUR 100,000, in each of the following categories:

• Logical Foundations of Mathematics,
• Logical Foundations of Computer Science, and
• Logical Foundations of Artificial Intelligence

The following three Boards of Jurors were in charge of choosing the winners:

• Logical Foundations of Mathematics: Jan Krajíček, Angus Macintyre, and Dana Scott (Chair).
• Logical Foundations of Computer Science: Franz Baader, Johann Makowsky, and Wolfgang Thomas (Chair).
• Logical Foundations of Artificial Intelligence: Luigia Carlucci Aiello, Georg Gottlob (Chair), and Bernhard Nebel.

http://fellowship.logic.at/

ABSTRACT. The aim of the FLoC Olympic Games is to start a tradition in the spirit of the ancient Olympic Games, a Panhellenic sport festival held every four years in the sanctuary of Olympia in Greece, this time in the scientific community of computational logic. Every four years, as part of the Federated Logic Conference, the Games will gather together all the challenging disciplines from a variety of computational logic in the form of the solver competitions.

At the Award Ceremonies, the competition organizers will have the opportunity to present their competitions to the public and give away special prizes, the prestigious Kurt Gödel medals, to their successful competitors. This reinforces the main goal of the FLoC Olympic Games, that is, to facilitate the visibility of the competitions associated with the conferences and workshops of the Federated Logic Conference during the Vienna Summer of Logic.

This award ceremony will host the

• 3rd Confluence Competition (CoCo 2014);
• Configurable SAT Solver Challenge (CSSC 2014);
• Ninth Max-SAT Evaluation (Max-SAT 2014);
• QBF Gallery 2014; and
• SAT Competition 2014 (SAT-COMP 2014).

ABSTRACT. Idris is a purely functional programming language with dependent types. As well as supporting theorem proving, Idris is intended to be a general purpose programming language. As such, it provides high-level concepts such as implicit syntax, type classes and "do" notation.

Many components of a dependently-typed programming language are by now well understood, for example the underlying type theory, type checking, unification and evaluation. How to combine these components into a realistic and usable high-level language is, however, folklore, discovered anew by successive language implementors. In this talk, I will give an overview of the implementation of Idris, showing how these it brings these components together into a complete programming language.

I will briefly describe the high-level language and the underlying type theory, and present a tactic-based method for elaborating concrete high-level syntax with implicit arguments and type classes into a fully explicit core type theory. Furthermore, I will show how this method facilitates the implementation of new high-level language constructs.

ABSTRACT. Weak ω-groupoids are the higher dimensional generalisation of setoids and are an essential ingredient of the constructive semantics of Homotopy Type Theory [10]. Following up on our previous formalisation [3] and Brunerie’s notes [5], we present a new formalisation of the syntax of weak ω-groupoids in Agda using heterogeneous equality. We show how to recover basic constructions on ω-groupoids using suspension and replacement. In particular we show that any type forms a groupoid and we outline how to derive higher dimensional composition. We present a possible semantics using globular sets and discuss the issues which arise when using globular types instead.

ABSTRACT. In [1], Allen Stoughton proposed a notion of substitution for the Lambda calculus formulated in its original syntax with only one sort of symbols (names) for variables --without identifying $\alpha$-convertible terms. According to such formulation, the action of substitution on terms is defined by simple structural recursion and an interesting theory arises concerning e.g. $\alpha$ conversion. In this paper we present a formalisation of Stoughton's development in Constructive Type Theory using the language Agda, up to the Substitution Lemma for $\alpha$ conversion. The code obtained is quite concise and we are able to formulate some improvements over the original presentation. For instance, our definition of $\alpha$ conversion is just syntax directed but we are nevertheless able to prove in an easy way that it gives rise to an equivalence relation, whereas in [1] the latter was included as part of the definition. As a result of this work we are inclined to assert that Stoughton's is the right way to formulate the Lambda calculus in its original, conventional syntax and that it is a formulation amenable to fully formal treatment.

[1] A. Stoughton. Substitution revisited. Theor. Comput. Sci., 59:317-325, 1988.