Author name cluster
Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.
LFMTP Workshop 2013 Conference Paper
We describe how the Davis-Putnam-Logemann-Loveland procedure DPLL is bisimilar to the goal-directed proof-search mechanism described by a standard but carefully chosen sequent calculus. We thus relate a procedure described as a transition system on states to the gradual completion of incomplete proof-trees.
I&C Journal 2012 Journal Article
This article has been withdrawn at the request of the author(s) and/or editor. The Publisher apologizes for any inconvenience this may cause. The full Elsevier Policy on Article Withdrawal can be found at http: //www. elsevier. com/locate/withdrawalpolicy.
CSL Conference 2011 Conference Paper
This paper revisits models of typed lambda calculus based on filters of intersection types: By using non-idempotent intersections, we simplify a methodology that produces modular proofs of strong normalisation based on filter models. Building such a model for some type theory shows that typed terms can be typed with intersections only, and are therefore strongly normalising. Non-idempotent intersections provide a decreasing measure proving a key termination property, simpler than the reducibility techniques used with idempotent intersections. Such filter models are shown to be captured by orthogonality techniques: we formalise an abstract notion of orthogonality model inspired by classical realisability, and express a filter model as one of its instances, along with two term-models (one of which captures a now common technique for strong normalisation). Applying the above range of model constructions to Curry-style System F describes at different levels of detail how the infinite polymorphism of System F can systematically be reduced to the finite polymorphism of intersection types.
I&C Journal 2009 Journal Article
We present the Lambda Context Calculus. This simple lambda-calculus features variables arranged in a hierarchy of strengths such that substitution of a strong variable does not avoid capture with respect to abstraction by a weaker variable. This allows the calculus to express both capture-avoiding and capturing substitution (instantiation). The reduction rules extend the ‘vanilla’ lambda-calculus in a simple and modular way and preserve the look and feel of a standard lambda-calculus with explicit substitutions. Good properties of the lambda-calculus are preserved. The LamCC is confluent, and a natural injection into the LamCC of the untyped lambda-calculus exists and preserves strong normalisation. We discuss the calculus and its design with full proofs. In the presence of the hierarchy of variables, functional binding splits into a functional abstraction λ (lambda) and a name-binder и (new). We investigate how the components of this calculus interact with each other and with the reduction rules, with examples. In two more extended case studies we demonstrate how global state can be expressed, and how contexts and contextual equivalence can be naturally internalised using function application.
I&C Journal 2007 Journal Article
We present a simple term calculus with an explicit control of erasure and duplication of substitutions, enjoying a sound and complete correspondence with the intuitionistic fragment of Linear Logic’s proof-nets. We show the operational behaviour of the calculus and some of its fundamental properties such as confluence, preservation of strong normalisation, strong normalisation of simply typed terms, step by step simulation of β-reduction and full composition.
CSL Conference 2006 Conference Paper
Abstract Based on natural deduction, Pure Type Systems ( PTS ) can express a wide range of type theories. In order to express proof-search in such theories, we introduce the Pure Type Sequent Calculi ( PTSC ) by enriching a sequent calculus due to Herbelin, adapted to proof-search and strongly related to natural deduction. PTSC are equipped with a normalisation procedure, adapted from Herbelin’s and defined by local rewrite rules as in Cut-elimination, using explicit substitutions. It satisfies Subject Reduction and it is confluent. A PTSC is logically equivalent to its corresponding PTS, and the former is strongly normalising if and only if the latter is. We show how the conversion rules can be incorporated inside logical rules (as in syntax-directed rules for type checking), so that basic proof-search tactics in type theory are merely the root-first application of our inference rules.
I&C Journal 2004 Journal Article
We present a new system of intersection types for a composition-free calculus of explicit substitutions with a rule for garbage collection, and show that it characterizes those terms which are strongly normalizing. This system extends previous work on the natural generalization of the classical intersection types system, which characterized head normalization and weak normalization, but was not complete for strong normalization. An important role is played by the notion of available variable in a term, which is a generalization of the classical notion of free variable.