View: session overviewtalk overviewside by side with other conferences
08:50  Welcome Remarks SPEAKER: Brigitte Pientka ABSTRACT. Welcome to the 9th International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP 2014. The LFMTP workshop series resulted from the amalgamation of the Logical Frameworks and Metalanguages (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 (CSLLICS), 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?. 
09:00  ProofTheoretic Foundations of Indexing in Logic Programming SPEAKER: Iliano Cervesato 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. 
09:25  Hybrid Extensions in a Logical Framework SPEAKER: Agata Murawska 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. 
09:50  Variable Arity for LF SPEAKER: John Boyland ABSTRACT. The dependentlytyped lambda calculus (LF) supports use of metalevel 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 fixedsize contexts. However, because LF does not have a concept of variablearity functions, a hypothetical judgment depending on a variablesize context cannot be modeled as an LF function. This paper extends LF to support variablearity 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 metamachinery 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 
10:45  Session Types Meet Separation Logic SPEAKER: Jesper Bengtson 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 postconditions 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 higherorder separation logic by extending a Javalike 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. 
11:45  Internal Adequacy of Bookkeeping in Coq SPEAKER: Ivan Scagnetto 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 wellknown 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 higherorder abstract syntax (HOAS), which allows us to deal smoothly with the representation of the universal binder of System F 
12:10  A Generic Approach to Proofs about Substitution SPEAKER: Abhishek Anand 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. 
12:35  A Framework for Implementing Logical Frameworks SPEAKER: Florian Rabe 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. 
14:30  A Framework for the Verified Transformation of Functional Programs SPEAKER: Gopalan Nadathur 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 theoremprover provide a natural framework for the verified implementation of such transformations. Underlying this argument is the fact that the transformations are syntaxdirected and rulebased, with the important proviso that they pay attention to and also modify the binding structure of programs. The logic of higherorder hereditary Harrop formulas, the HoHH logic for short, is wellsuited to formalizing such descriptions especially because of the support it provides for the higherorder 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 higherorder 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. 
15:20  Automatically Deriving Schematic Theorems for Dynamic Contexts SPEAKER: Olivier Savary Bélanger ABSTRACT. Hypothetical judgments go handinhand with higherorder abstract syntax for metatheoretic 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 coinductive 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. 
16:30  Foundations and Technology Competitions Award Ceremony 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:
The following three Boards of Jurors were in charge of choosing the winners:
http://fellowship.logic.at/ 
17:30  FLoC Olympic Games Award Ceremony 1 SPEAKER: Floc Olympic Games 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

18:15  FLoC Closing Week 1 SPEAKER: Helmut Veith 
16:30  Idris: Implementing a Dependently Typed Programming Language SPEAKER: Edwin Brady 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 highlevel concepts such as implicit syntax, type classes and "do" notation. Many components of a dependentlytyped 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 highlevel 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 highlevel language and the underlying type theory, and present a tacticbased method for elaborating concrete highlevel 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 highlevel language constructs. 