Published: 3rd July 2018|
|Invited Talk: Cubical Computational Type Theory and RedPRL Kuen-Bang Hou (Favonia)|
|Invited Talk: A Fresh View of Call-by-Need Delia Kesner|
|Invited Talk: Why and How Does K Work? The Logical Infrastructure Behind It Grigore Rosu|
|The RedPRL Proof Assistant (Invited Paper) Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou (Favonia), Robert Harper and Jonathan Sterling||1|
|Formalisation in Constructive Type Theory of Barendregt's Variable Convention for Generic Structures with Binders Ernesto Copello, Nora Szasz and Álvaro Tasistro||11|
|Formalization in Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using Multiple Substitution Martín Copes, Nora Szasz and Álvaro Tasistro||27|
|Abstract Representation of Binders in OCaml using the Bindlib Library Rodolphe Lepigre and Christophe Raffalli||42|
|Sharing a Library between Proof Assistants: Reaching out to the HOL Family François Thiré||57|
This volume contains a selection of papers presented at LFMTP 2018, the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), held on July 7, 2018, in Oxford, UK. The workshop was affiliated with the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD) within the 7th Federated Logic Conference (FLoC).
Logical frameworks and meta-languages form a common substrate for representing, implementing and reasoning about a wide variety of deductive systems of interest in logic and computer science. Their design, implementation and their use in reasoning tasks, ranging from the correctness of software to the properties of formal systems, have been the focus of considerable research over the last two decades. This workshop brought together designers, implementors and practitioners to discuss various aspects impinging on the structure and utility of logical frameworks, including the treatment of variable binding, inductive and co-inductive reasoning techniques and the expressiveness and lucidity of the reasoning process.
We received 13 submissions in total, which were reviewed by at least 3 program committee members or external reviewers. Out of those, 4 were selected for presentation and 4 were selected for presentation and publication. These proceedings include the latter 4 plus one invited submission.
In addition to the submission presentations, the program included 3 invited talks by Delia Kesner (IRIF, CNRS and Université Paris Diderot, France), Kuen-Bang Hou (Favonia) (Institute for Advanced Study, Princeton, USA), and Grigore Rosu (University of Illinois at Urbana-Champaign, USA).
Many people have contributed to the success of LFMTP'18. We would like to thank the organization of FLoC for providing the infrastructure and coordination with other events. We are grateful for the great program committee who submitted all reviews on time and participated actively on the decisions. The authors and invited speakers are the ones responsible for a very interesting program, and the attendees for fruitful and stimulating discussions.Frédéric Blanqui & Giselle Reis May 31, 2018
(Joint work with Carlo Angiuli, Evan Cavallo, Robert Harper and Jonathan Sterling) Recent research revealed the deep connection between type theory and homotopy theory, which inspired a series of new type theories. The characteristic new features are univalence and higher inductive types, which have led to a fruitful development of synthetic homotopy theory. Unfortunately, those new features were originally introduced as axioms and disrupted the computational content of type theory, which affects their practicality in mechanizing proofs. To date, the most promising approach to enjoy new features inspired by homotopy theory while retaining computational content is through cubical structure. Cohen et al. constructed a type theory based on De Morgan cubes with both univalence and higher inductive types. Influenced by their work, we also built a type-theoretic semantics with all the features, but instead based on Cartesian cubes. In addition to using a different cubical structure, our semantics is built from computational content directly, following a computation-first methodology which itself is interesting. RedPRL is our first proof assistant based on the new semantics, inheriting the PRL style pioneered by the Nuprl proof assistant, which is also based on the computation-first methodology (but without cubical structure). We are also developing different proof assistants with distinct proof theories, in hope to create the best tools for mechanizing homotopy theory and other mathematics. In this talk, I will describe how the computation-first methodology works, compare two cubical type theories and discuss RedPRL.
Call-by-need is a lazy evaluation strategy which overwrites an argument with its value the first time it is evaluated, thus avoiding a costly re-evaluation mechanism. It is used in functional programming languages like Haskell and Miranda. In this talk we present a fresh view of call-by-need in three different aspects:
The K framework was born from our firm
belief that an ideal language framework is possible. Specifically, that
programming languages must have formal definitions, and that tools for a given
language, such as interpreters, compilers, state-space explorers, model
checkers, deductive program verifiers, etc., are derived from just one reference
formal definition of the language, correct-by-construction and at no additional
cost specific to that language. No other semantics for the same language should
be needed. Several real languages have been formalized their semantics in K,
VM (EVM), and the generic K tools have been instantiated to with these
languages. In particular, the EVM semantics is used commercially by Runtime Verification to formally
verify smart contracts on the Ethereum blockchain.
But what is behind K? Why and how does it work? This talk will discuss the logical formalism underlying K, matching logic, a first-order logic (FOL) variant for specifying and reasoning about structure by means of patterns and pattern matching. Matching logic generalizes several logical frameworks important for program analysis, such as: propositional logic, algebraic specification, FOL with equality, (polyadic) modal logics, temporal logics, separation logic, as well as dynamic and Hoare logics. Binders and fixed-points can also be defined in matching logic, and thus the variety of lambda/mu-calculi and substitution-based semantics. Patterns can specify both structural requirements, including separation requirements at any level in any program configuration (not only in the "heap"), as well as logical requirements and constraints. The various languages defined in K, regardless of their size and complexity, become nothing but matching logic theories, and the various tools provided by the K framework, such as interpretation, symbolic execution, search and model checking, as well as full-fledged deductive program verification, become nothing but proof search heuristics in matching logic.