Meta-CLF

Project Description

People

• Iliano Cervesato
• Frank Pfenning
• Jorge Sacchini

Collaborators

• Henry DeYoung
• Chris Martens
• Rob Simmons
• Carsten Schürmann
• Ian Voysey
• Elizabeth Davis

Past members

• Beniamino Accattoli
• Yuxin Deng
• Kristina Sojakova
• Anand Subramanian
• Bernardo Toninho

• Yuxin Deng, Iliano Cervesato and Rob Simmons: Relating reasoning methodologies in linear logic and process algebra, Mathematical Structures in Computer Science — MSCS, vol. -1, pp.1-39, December 2014.
  We show that the proof-theoretic notion of logical preorder coincides with the process-theoretic notion of barbed preorder for a CCS-like process calculus obtained from the formula-as-process interpretation of a fragment of linear logic. The argument makes use of other standard notions in process algebra, namely simulation and labeled transition systems. This result establishes a connection between an approach to reason about process specifications, the barbed preorder, and a method to reason about logic specifications, the logical preorder.
• Jorge Luis Sacchini, Iliano Cervesato, Frank Pfenning and Carsten Schürmann: Mode checking in the Concurrent Logical Framework, Technical Report CMU-CS-14-134, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, August 2014.
  We define and prove correct a mode checker for a significant fragment of the concurrent logical framework CLF.
• Elizabeth Davis: A Proof-Based Approach to Formalizing Protocols in Linear Epistemic Logic, Senior Research Honors Thesis, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, May 2014.
  Linear epistemic logic can be used to reason about changing knowledge states of agents acting in a system. Here we use it to formalize the Needham-Schröder-Lowe public-key authentication protocol for establishing secure communication sessions. We have developed a notion of adequacy to refer to the formal compositional correspondence between the protocol and the formalism. Through the iterative process of attempting to prove adequacy theorems and noting where and how the proof breaks down, we have been able to refine the formalism so that it adheres to the structure and semantics of the protocol as it was originally specified. This work is the first step towards showing that rigorous formal reasoning can be applied to protocols and processes followed in the wild.

• Iliano Cervesato and Jorge Luis Sacchini: Towards Meta-Reasoning in the Concurrent Logical Framework CLF, Combined 20th International Workshop on Expressiveness in Concurrency and 10th Workshop on Structural Operational Semantics — EXPRESS/SOS'13 (Johannes Borgström and Bas Luttik, editors), Buenos Aires, Argentina, August 2013.
  The concurrent logical framework CLF is an extension of the logical framework LF designed to specify concurrent and distributed languages. While it can be used to define a variety of formalisms, reasoning about such languages within CLF has proved elusive. In this paper, we propose an extension of LF that allows us to express properties of CLF specifications. We illustrate the approach with a proof of safety for a small language with a parallel semantics.
• Jorge Luis Sacchini: Type-Based Productivity of Stream Definitions in the Calculus of Constructions, 28th Annual ACM/IEEE Symposium on Logic In Computer Science — LICS'13 (Orna Kupferman, editor), New Orleans, USA, June 25-28, 2013.
  Productivity of corecursive definitions is an essential property in proof assistants since it ensures logical consistency and decidability of type checking. Type-based mechanisms for ensuring productivity use types annotated with size information to track the number of elements produced in corecursive definitions. In this paper, we propose an extension of the Calculus of Constructions—the theory underlying the Coq proof assistant—with a type-based criterion for ensuring productivity of stream definitions. We prove strong normalization and logical consistency. Furthermore, we define an algorithm for inferring size annotations in types. These results can be easily extended to handle general coinductive types.
• Beniamino Accattoli: Compressing polarized boxes, 28th Annual ACM/IEEE Symposium on Logic In Computer Science — LICS'13 (Orna Kupferman, editor), New Orleans, USA, June 25-28, 2013.
  The sequential nature of sequent calculus provides a simple definition of cut-elimination rules that duplicate or erase sub-proofs. The parallel nature of proof nets, instead, requires the introduction of explicit boxes, which are global and synchronous constraints on the structure of graphs. We show that logical polarity can be exploited to obtain an implicit, compact, and natural representation of boxes: in an expressive polarized dialect of linear logic, boxes may be represented by simply recording some of the polarity changes occurring in the box at level 0. The content of the box can then be recovered locally and unambiguously. Moreover, implicit boxes are more parallel than explicit boxes, as they realize a larger quotient. We provide a correctness criterion and study the novel and subtle cut-elimination dynamics induced by implicit boxes, proving confluence and strong normalization.
• Beniamino Accattoli: Linear logic and strong normalization, 24th International Conference on Rewriting Techniques and Applications — RTA'13 (Femke van Raamsdonk, editor), Eindhoven, the Netherlands, June 24-26, 2013. (Best paper award.)
  Strong normalization for linear logic requires elaborated rewriting techniques. In this paper we give a new presentation of MELL proof nets, without any commutative cut-elimination rule. We show how this feature induces a compact and simple proof of strong normalization, via reducibility candidates. It is the first proof of strong normalization for MELL which does not rely on any form of confluence, and so it smoothly scales up to full linear logic. Moreover, it is an axiomatic proof, as more generally it holds for every set of rewriting rules satisfying three very natural requirements with respect to substitution, commutation with promotion, full composition, and Kesner's IE property. The insight indeed comes from the theory of explicit substitutions, and from looking at the exponentials as a substitution device.
• Yuxin Deng and Matthew Hennessy: On the Semantics of Markov Automata, in Information & Computation, vol. 222, pp.139-168, 2013.
  Markov automata describe systems in terms of events which may be nondeterministic, may occur probabilistically, or may be subject to time delays. We define a novel notion of weak bisimulation for such systems and prove that this provides both a sound and complete proof methodology for a natural extensional behavioural equivalence between such systems, a generalisation of reduction barbed congruence, the well-known touchstone equivalence for a large variety of process description languages.
• Beniamino Accattoli: Evaluating functions as processes, 7th International Workshop on Computing with Terms and Graphs — TERMGRAPH'13 (Rachid Echahed and Detlef Plump, editors), Rome, Italy, March 23, 2013.
  A famous result by Milner is that the λ-calculus can be simulated inside the π-calculus. This simulation, however, holds only modulo strong bisimilarity on processes, i.e. there is a slight mismatch between β-reduction and how it is simulated in the π-calculus. The idea is that evaluating a λ-term in the π-calculus is like running an environment-based abstract machine, rather than applying ordinary β-reduction. In this paper we show that such an abstract-machine evaluation corresponds to linear weak head reduction, a strategy arising from the representation of λ-terms as linear logic proof nets, and that the relation between the two is as tight as it can be. The study is also smoothly rephrased in the call-by-value case, introducing a call-by-value analogous of linear weak head reduction.

• Iliano Cervesato, Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann and Rob Simmons: Trace Matching in a Concurrent Logical Framework, 7th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice — LFMTP'12 (Adam Chlipala and Carsten Schürmann, editors), Copenhagen, Denmark, September 2012.
  Matching is an important component of a logical framework. It is at the heart of many reasoning tasks and underlies the operational semantic for well moded logic programs. We study the problem of matching on concurrent traces in the CLF logical framework, an extension of LF that supports the specification of concurrent and distributed systems. A concurrent trace is a sequence of computations where independent steps can be permuted. We give a sound and complete algorithm for matching traces with one variable standing for an unknown subtrace.
• Iliano Cervesato, Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann and Rob Simmons: On Matching in CLF, Technical Report CMU-CS-12-114, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, July 2012.
  Matching is an important component of a logical framework. It is at the heart of many reasoning tasks and is sufficient to support the operational semantic of well-moded logic programs. Matching is poorly understood for logical frameworks such as CLF, designed to effectively capture the specifications of parallel, concurrent and distributed systems. The witnesses of their computations, and therefore their term language, are concurrent traces. A concurrent trace is a sequence of computations where independent steps can be permuted. We study the problems of matching concurrent traces on large fragments of CLF. Specifically, we give a sound and complete algorithm for matching traces with a single variable standing for an unknown subtrace. We also examine the unification problem for some simple fragments of CLF and give an algorithm for solving unification problems with with one variable standing for an unknown subtrace on each side of the equation.
• Iliano Cervesato: An Improved Proof-Theoretic Compilation of Logic Programs, Theory and Practice of Logic Programming – TPLP, vol. 12(4-5) (Agostino Dovier and Vítor Santos Costa, editors), pp 639-657, Cambridge University Press 2012. Special issue of the 28th International Conference on Logic Programming — ICLP'12, Budapest, Hungary, September 2012,
  In prior work, we showed that logic programming compilation can be given a proof-theoretic justification for generic abstract logic programming languages, and demonstrated this technique in the case of hereditary Harrop formulas and their linear variant. Compiled clauses were themselves logic formulas except for the presence of a second-order abstraction over the atomic goals matching their head. In this paper, we revisit our previous results into a more detailed and fully logical justification that does away with this spurious abstraction. We then refine the resulting technique to support well-moded programs efficiently.
• Iliano Cervesato, Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann and Rob Simmons: On Matching Concurrent Traces, 26th International Workshop on Unification — UNIF'12 (Santiago Escobar, Konstantin Korovin and Vladimir Rybakov, editors), Manchester, UK, July 2012.
  Concurrent traces are sequences of computational steps where independent steps can be permuted and executed in any order. We study the problem of matching on concurrent traces. We outline a sound and complete algorithm for matching traces with one variable standing for an unknown subtrace.
• Yuxin Deng and Alwen Tiu: Characterisations of testing preorders for a finite probabilistic π-calculus, Formal Aspects of Computing Volume 24, Numbers 4-6 (2012), pp. 701-726.
  We consider two characterisations of the may and must testing preorders for a probabilistic extension of the finite π-calculus: one based on notions of probabilistic weak simulations, and the other on a probabilistic extension of a fragment of Milner-Parrow-Walker modal logic for the π-calculus. We base our notions of simulations on similar concepts used in previous work for probabilistic CSP. However, unlike the case with CSP (or other non-value-passing calculi), there are several possible definitions of simulation for the probabilistic π-calculus, which arise from different ways of scoping the name quantification. We show that in order to capture the testing preorders, one needs to use the "earliest" simulation relation (in analogy to the notion of early (bi)simulation in the non-probabilistic case). The key ideas in both characterisations are the notion of a "characteristic formula" of a probabilistic process, and the notion of a "characteristic test" for a formula. As in an earlier work on testing equivalence for the π-calculus by Boreale and De Nicola, we extend the language of the π-calculus with a mismatch operator, without which the formulation of a characteristic test will not be possible.
• Steve Awodey, Nicola Gambino and Kristina Sojakova: Inductive Types in Homotopy Type Theory, Twenty-Seventh Annual ACM/IEEE Symposium on Logic In Computer Science — LICS'12 (Nachum Dershowitz, editor), Dubrovnik, Croatia, 25-28 June 2012.
  
  
  Homotopy type theory is an interpretation of Martin-Löf's constructive type theory into abstract homotopy theory. There results a link between constructive mathematics and algebraic topology, providing topological semantics for intensional systems of type theory as well as a computational approach to algebraic topology via type theory-based proof assistants such as Coq.
  The present work investigates inductive types in this setting. Modified rules for inductive types, including types of well-founded trees, or W-types, are presented, and the basic homotopical semantics of such types are determined. Proofs of all results have been formally verified by the Coq proof assistant, and the proof scripts for this verification form an essential component of this research.
• Yuxin Deng, Iliano Cervesato and Rob Simmons: Relating Reasoning Methodologies in Linear Logic and Process Algebra, Second International Workshop on Linearity — LINEARITY'12 (Sandra Alves and Ian Mackie, editors), Tallinn, Estonia, 1 April 2012.
  We show that the proof-theoretic notion of logical preorder coincides with the process-theoretic notion of contextual preorder for a CCS-like calculus obtained from the formula-as-process interpretation of a fragment of linear logic. The argument makes use of other standard notions in process algebra, namely a labeled transition system and a coinductively defined simulation relation. This result establishes a connection between an approach to reason about process specifications and a method to reason about logic specifications.