LINC (a logic with lambda terms, nabla, induction and co-induction)

08/24/04

Home
Publications
Downloads
People
Feedback

 

The logic Linc is an extension of first-order intuitionistic logic aimed at providing a framework for specifying and reasoning about computation systems. The basic idea is to encode computation as deduction. Evaluation of a computation expressions (programs) is mapped to proof search. Reasoning about computations (proofs) can therefore benefit from its logical structures.

Several keywords that best describe our approach here: operational semantics, lambda-tree syntax, proof search, (higher-order pattern) unification. We focus on the representation of computation system as deductive systems, e.g., structured operational semantics or natural semantics. We use lambda-tree syntax (or higher-order abstract syntax) to encode terms in computation systems. This style of encoding uses lambda-abstraction to represent binding structures in the computation systems and beta-reduction to model substitution. Unification on lambda-terms is used in proof search, for example, in backchaining, to instantiate variables lazily. This allows one to encode symbolic execution of some specifications of computation systems.

This website contains various materials related to the logic Linc and its application. In particular, you will find papers about the logic, implementations of various fragments of Linc and applications of these fragments to encode various computation systems. The logic Linc was developed by Alwen Tiu, in collaboration with Dale Miller (INRIA Futurs/Ecole polytechnique) and Alberto Momigliano (LFCS, University of Edinburgh).  It is part of the larger project, Parsifal, at INRIA Futurs.

We have recently implemented an automated prover for reasoning about process calculi. One of the applications is in encoding π-calculus and open bisimulation, a proof method for reasoning about process equivalence. Details of the encoding can be found in this paper, and its implementation is described here.

Home | Publications | Downloads | People | Feedback

Last updated 08/24/04 by Alwen Tiu (tiu at lix.polytechnique.fr)