LINC (a logic with lambda terms, nabla, induction and coinduction)  
08/24/04 

The logic Linc is an extension of firstorder 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, lambdatree syntax, proof search, (higherorder pattern) unification. We focus on the representation of computation system as deductive systems, e.g., structured operational semantics or natural semantics. We use lambdatree syntax (or higherorder abstract syntax) to encode terms in computation systems. This style of encoding uses lambdaabstraction to represent binding structures in the computation systems and betareduction to model substitution. Unification on lambdaterms 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. 
Last updated 08/24/04 by Alwen Tiu (tiu at lix.polytechnique.fr)