Programme

Friday 18th November 2011

10:00 – 10:15

Welcome

10:15 – 11:15

Jamie Gabbay

Proof-theory for meta-programming and modal type theory

Calculi based on intuitionistic S4 are a basis for certain kinds of meta-programming, as has been observed by Nanevski and colleagues. I propose to describe a simplified presentation of this work, developed with Nanevski, and a denotational semantics for it.
The interest is twofold: it gives a semantics for intuitionistic S4 and thus specifically an interesting denotational interpretation of the Box modality and operational interpretations of its theorems; and it gives a denotational semantics for a style of meta-programmin based on a rigorous analysis of modal type theory.

Didier Galmiche

Label-free Natural Deduction Systems for intuitionistic modal logics

In this talk we present natural deduction for the intuitionistic and classical (normal) modal logics obtained from the combinations of the axioms T , B, 4 and 5. In this context we introduce a new multi-contextual structure, called T-sequent, that allows to design simple label- free natural deduction systems for these logics. After proving that they are sound and complete we show that they satisfy the normalization property and consequently the sub-formula property in the intuitionistic case.
This is a joint work with Yakoub Salhi.

11:15 – 11:30

Break

11:30 – 12:30

Mehrnoosh Sadrzadeh

Algebra and Proof Theory for a Logic of Propositions, Actions and Adjoint Modal Operators

We develop a cut-free nested sequent calculus as basis for a proof search procedure for a modal logic of actions and propositions. The actions act on a logic of propositions via a dynamic modality (the weakest precondition of program logics), whose left adjoint we refer to as 'update' (the strongest postcondition). Both logics are positive and have agent-indexed adjoint pairs of epistemic modalities: the left adjoints encode agents' uncertainties and the right adjoints encode their beliefs. We prove admissibility of Cut, and hence the soundness and completeness of the logic with regard to an algebraic semantics. We interpret the logic on epistemic scenarios that consist of honest and dishonest communication actions, add assumption rules to encode them, and prove that the calculus with the assumption rules still has the admissibility results. We apply our calculus to encode and solve the classic epistemic puzzle of muddy children and a modern version of it with dishonest children.

Marta Bilkova - Jiri Velebil

Substructural logics are coalgebraic

A slogan says that modal logics are coalgebraic (analogous to: equational logics are algebraic). So far, the methods of universal coalgebra have been applied to various types of classical modal logics. We want to show that substructural logics (including intutionistic logic) are coalgebraic as well.
We define the category of ``distributive substructural frames'' and prove that these frames can be considered as a class of coalgebras for a locally monotone endofunctor of preorders. In fact, the above class of frames is modally definable, the modal algebras being precisely the residuated distributive lattices.
This is a joint work with Rostislav Horcik.

12:30 – 14:15

Lunch

14:15 – 15:15

Vladimir Komendantsky

Verification of functional programs in higher order type theory and Coq

We present a type theoretic view to the problem of verification of pattern matching algorithms taking as examples regular expression matching, containment and equivalence. We consider the case when such an algorithm is written as a structurally recursive, terminating functional program. Higher order type theory allows us to encode both the computational content and also logical properties of the algorithm. The latter gives the programmer an incite into why the algorithm indeed computes what it is supposed to, apart from the usual assurance of correctness.

Jael Kriener

Formalising a Determinacy Analysis for Prolog in Coq

I have recently presented a contextual semantics for Prolog programs containing 'cut' and a static analysis such programs that infers deterministic modes of predicates and proved the latter correct with respect to the former. I will present here my efforts to formalize this prove in Coq.

15:15 – 15:30

Break

15:30 – 16:30

Nordstrom Bengt

Towards a basis for human-computer dialogues

A dialogue is seen as the refinement of a mathematical object. The syntactic well-formedness of the dialogue (like you have to give both departure and arrival dates when ordering a hotel or you cannot order surströmming in an English restaurant) is then expressed using dependent types.
This is based on work with interactive proof editors for Type Theory.

Peter Foldiak

Neural representation and categories

The neural code maps states of the environment or states of 'mind' to the electrical activity patterns of neurons. There is evidence that the brain uses a sparse and explicit neural code, meaning that each state is coded by the activity of a small fraction of available neurons, and that neurons represent semantically interpretable aspects of the state. The overlap of the codewords then imply semantic relationships between the represented items. This structure within the code is well captured by Formal Concept Analysis (FCA), where objects are the items to be represented and the attributes are the neurons activated by the items. FCA and its statistical extension are useful tools for representing categories in a flexible way.

16:30 – 17:00

Break

17:00 – 19:00 Reception

19:00 – ... Dinner in local restaurant Number 40, The Scores, St. Andrews, KY16 9AS

View Larger Map

Saturday 19th November 2011

09:30 – 10:30

James McKinna

From proof theory to HCI and back again

The research programme of mechanising logic has more often than not emphasised the proof theory over interaction design. In this talk I want to sketch a more fruitful synthesis, illustrated by the work done in recent years by Stephane, Roy and myself on proof search in the setting of Pure Type Systems.

Luís Pinto

Normal forms in sequent calculus

In sequent calculus, traditionally, normal forms are taken to be the cut-free derivations, and not much attention is paid to the interaction between cut-elimination and permutative conversions. Nonetheless, the class of cut-free derivations is known to exhibit redundancies, when mapped into natural deduction. In particular, Mints and Dyckhoff-Pinto, independently, identified a class of “normal cut-free” derivations in bijection with normal natural deductions, which arises as the class of normal forms w.r.t. certain permutative conversions.
In this talk, we present work on the interaction between cut-elimination and permutative conversions in a termed sequent calculus named lambda-Jm. This system corresponds to an extension with cuts of the multiary sequent calculus that Schwichtenberg introduced to prove termination of the rewriting system induced by the permutative conversions considered by Dyckhoff-Pinto.
We will survey the basic ideas and meta-theory of lambda-Jm, and pay special attention to normal forms resulting from combining permutative conversions and cut-elimination rules. Some of these combinations induce rewriting systems that allow for simulation of non-terminating reduction sequences known from explicit substitution calculi. Other combinations induce confluent and terminating rewriting systems whose normal forms correspond to interesting classes of terms: (i) the class of beta-normal terms of the ordinary lambda-calculus, (ii) the class of cut-free terms of Herbelin’s lambda-bar-calculus, and (iii) the class of Mints and Dyckhoff-Pinto’s normal cut-free forms. These classes are all in bijection, and reflect the existence in lambda-Jm of three alternatives to represent multiple application, i.e. application of a function to more than one argument. In the three rewriting systems, computation to normal form can be organised into two stages, so that the f irst stage consists of beta-normalisation (elimination of principal cuts) and focusing, and the second stage consists of choosing the representation of multiple application.
(Joint work with José Espírito Santo and Maria João Frade.)

10:30 – 11:00

Break

11:00 – 12:30

Christian Urban

Formalising Regular Language Theory with Regular Expressions Only

There are numerous textbooks on regular languages. Nearly all of them introduce the subject by describing finite automata and only mentioning on the side a connection with regular expressions. Unfortunately, automata are difficult to formalise theorem provers. The reason is that they need to be represented as graphs, matrices or functions, none of which are inductive datatypes. Also convenient operations for disjoint unions of graphs, matrices and functions are not easily formalisiable. In contrast, regular expressions can be defined conveniently as a datatype and a corresponding reasoning infrastructure comes for free. I will show in this talk that a central result from formal language theory - the Myhill-Nerode Theorem - can be recreated using only regular expressions. From this theorem many closure properties of regular languages follow.

William Stirton

Polymorphically typed combinatory logic

At present, so far as I know, no such thing as a polymorphically typed combinatory calculus exists in print. Indeed, because of the quantified types, the task of formulating one which is equivalent to the familiar polymorphically typed lambda calculus is non-trivial. I will formulate a polymorphically typed combinatory calculus and prove that it is "equivalent" to the familiar polymorphically typed lambda calculus in a sense of "equivalent" that will be defined.
This calculus is of interest, of course, only in so far as it facilitates the proving of interesting metatheoretical results. I will review some of the proof-theoretical results that exist relating to the polymorphically typed lambda calculus, by Leivant, Coquand, Altenkirch and Aehlig. Special emphasis will be placed upon the fact that there is a subsystem of the calculus just strong enough to represent the primitive recursive functionals of finite type. There is at least one important question relating to this subsystem - how many contractions are needed to normalize a term? - to which no published answer has yet been given. Although it will not be possible to present my solution in detail, there are reasons for thinking that it is much easier to answer this question in relation to the combinatory calculus than in relation to the lambda calculus (by direct methods at least).
Some of the foregoing has been submitted to the Archive for Mathematical Logic (and the referees recommended revisions and resubmission); but the proof of equivalence mentioned in the first paragraph above is new.

Natasha Alechina

The logic of joint action

This talk is about expressing coalitional ability (as in Coalition Logic CL) in a PDL-like logic with intersection of modalities. To be precise, we study multi-modal $K$ with intersection of modalities, interpreted over models corresponding to game structures, and give a complete axiomatisation as well as a characterisation of key complexity problems. This is joint work with Thomas Agotnes.

12:30 – 14:00

Lunch

14:00 – 15:00

Sara Negri

The geometry of proof analysis: From rule systems to systems of rules

In the program of proof analysis, what are called geometric implications in categorical logic are converted into sequent calculus rules with eigenvariable conditions. This method makes it possible to convert into rules e.g. existence axioms. A generalization is proposed into a situation with several rules with eigenvariables, applied in a specific succession. The corresponding class of axioms arose from a concrete situation of proof analysis met in epistemic logic.

Stephen Read

On GE-harmony

Michael Dummett introduced the notion of harmony in response to Arthur Prior's tonkish attack on the idea of proof-theoretic justification of logical laws (or analytic validity). But Dummett vacillated between different conceptions of harmony, in an attempt to use the idea to underpin his anti-realism. Dag Prawitz had already articulated an idea of Gerhard Gentzen's into a procedure whereby elimination-rules are in some sense functions of the corresponding introduction-rules. Roy Dyckhoff, in a joint paper with Nissim Francez, `A note on harmony', finally published this year, coined the term ''general-elimination harmony'' for the relationship created by this procedure. In this talk I want to open up for discussion ways in which Roy's and my own conception of GE-harmony to some extent differ.

15:00 – 15:30

Break

15:30 – 16:30

Peter Schroeder-Heister

Proof-theoretic semantics, self-contradition, and the format of deductive reasoning

From the point of view of proof-theoretic semantics, I argue that the sequent calculus with introduction rules both on the assertion and on the assumption side represents deductive reasoning more appropriately than natural deduction. In taking consequence to be conceptually prior to truth, it can deal with non-well-founded phenomena such as contradictory reasoning. The fact that in its typed variant, the sequent calculus has an explicit and separable substitution schema in form of the cut rule, is seen as a crucial advantage over natural deduction, where substitution is built into the general framework.

Rob Rothenberg

On Labelled Sequents and Hypersequents

It is part of the folklore of hypersequent calculi that they are equivalent to labelled calculi. We give an overview of recent work on the translation of proofs between formalisms that labelled calculi with relations are more expressive, meaning that there is no 1-1 translation. However, we do show that some proofs in labelled calculi can be translated into hypersequent calculi for logics with linearity.

19:00 – ... For those who are still here, dinner together

10:00 – 10:15	Welcome
10:15 – 11:15	Jamie Gabbay	Proof-theory for meta-programming and modal type theory Calculi based on intuitionistic S4 are a basis for certain kinds of meta-programming, as has been observed by Nanevski and colleagues. I propose to describe a simplified presentation of this work, developed with Nanevski, and a denotational semantics for it. The interest is twofold: it gives a semantics for intuitionistic S4 and thus specifically an interesting denotational interpretation of the Box modality and operational interpretations of its theorems; and it gives a denotational semantics for a style of meta-programmin based on a rigorous analysis of modal type theory.
	Didier Galmiche	Label-free Natural Deduction Systems for intuitionistic modal logics In this talk we present natural deduction for the intuitionistic and classical (normal) modal logics obtained from the combinations of the axioms T , B, 4 and 5. In this context we introduce a new multi-contextual structure, called T-sequent, that allows to design simple label- free natural deduction systems for these logics. After proving that they are sound and complete we show that they satisfy the normalization property and consequently the sub-formula property in the intuitionistic case. This is a joint work with Yakoub Salhi.
11:15 – 11:30	Break
11:30 – 12:30	Mehrnoosh Sadrzadeh	Algebra and Proof Theory for a Logic of Propositions, Actions and Adjoint Modal Operators We develop a cut-free nested sequent calculus as basis for a proof search procedure for a modal logic of actions and propositions. The actions act on a logic of propositions via a dynamic modality (the weakest precondition of program logics), whose left adjoint we refer to as 'update' (the strongest postcondition). Both logics are positive and have agent-indexed adjoint pairs of epistemic modalities: the left adjoints encode agents' uncertainties and the right adjoints encode their beliefs. We prove admissibility of Cut, and hence the soundness and completeness of the logic with regard to an algebraic semantics. We interpret the logic on epistemic scenarios that consist of honest and dishonest communication actions, add assumption rules to encode them, and prove that the calculus with the assumption rules still has the admissibility results. We apply our calculus to encode and solve the classic epistemic puzzle of muddy children and a modern version of it with dishonest children.
	Marta Bilkova - Jiri Velebil	Substructural logics are coalgebraic A slogan says that modal logics are coalgebraic (analogous to: equational logics are algebraic). So far, the methods of universal coalgebra have been applied to various types of classical modal logics. We want to show that substructural logics (including intutionistic logic) are coalgebraic as well. We define the category of ``distributive substructural frames'' and prove that these frames can be considered as a class of coalgebras for a locally monotone endofunctor of preorders. In fact, the above class of frames is modally definable, the modal algebras being precisely the residuated distributive lattices. This is a joint work with Rostislav Horcik.
12:30 – 14:15	Lunch
14:15 – 15:15	Vladimir Komendantsky	Verification of functional programs in higher order type theory and Coq We present a type theoretic view to the problem of verification of pattern matching algorithms taking as examples regular expression matching, containment and equivalence. We consider the case when such an algorithm is written as a structurally recursive, terminating functional program. Higher order type theory allows us to encode both the computational content and also logical properties of the algorithm. The latter gives the programmer an incite into why the algorithm indeed computes what it is supposed to, apart from the usual assurance of correctness.
	Jael Kriener	Formalising a Determinacy Analysis for Prolog in Coq I have recently presented a contextual semantics for Prolog programs containing 'cut' and a static analysis such programs that infers deterministic modes of predicates and proved the latter correct with respect to the former. I will present here my efforts to formalize this prove in Coq.
15:15 – 15:30	Break
15:30 – 16:30	Nordstrom Bengt	Towards a basis for human-computer dialogues A dialogue is seen as the refinement of a mathematical object. The syntactic well-formedness of the dialogue (like you have to give both departure and arrival dates when ordering a hotel or you cannot order surströmming in an English restaurant) is then expressed using dependent types. This is based on work with interactive proof editors for Type Theory.
	Peter Foldiak	Neural representation and categories The neural code maps states of the environment or states of 'mind' to the electrical activity patterns of neurons. There is evidence that the brain uses a sparse and explicit neural code, meaning that each state is coded by the activity of a small fraction of available neurons, and that neurons represent semantically interpretable aspects of the state. The overlap of the codewords then imply semantic relationships between the represented items. This structure within the code is well captured by Formal Concept Analysis (FCA), where objects are the items to be represented and the attributes are the neurons activated by the items. FCA and its statistical extension are useful tools for representing categories in a flexible way.
16:30 – 17:00	Break
17:00 – 19:00	Reception
19:00 – ...	Dinner in local restaurant	Number 40, The Scores, St. Andrews, KY16 9AS View Larger Map

09:30 – 10:30	James McKinna	From proof theory to HCI and back again The research programme of mechanising logic has more often than not emphasised the proof theory over interaction design. In this talk I want to sketch a more fruitful synthesis, illustrated by the work done in recent years by Stephane, Roy and myself on proof search in the setting of Pure Type Systems.
	Luís Pinto	Normal forms in sequent calculus In sequent calculus, traditionally, normal forms are taken to be the cut-free derivations, and not much attention is paid to the interaction between cut-elimination and permutative conversions. Nonetheless, the class of cut-free derivations is known to exhibit redundancies, when mapped into natural deduction. In particular, Mints and Dyckhoff-Pinto, independently, identified a class of “normal cut-free” derivations in bijection with normal natural deductions, which arises as the class of normal forms w.r.t. certain permutative conversions. In this talk, we present work on the interaction between cut-elimination and permutative conversions in a termed sequent calculus named lambda-Jm. This system corresponds to an extension with cuts of the multiary sequent calculus that Schwichtenberg introduced to prove termination of the rewriting system induced by the permutative conversions considered by Dyckhoff-Pinto. We will survey the basic ideas and meta-theory of lambda-Jm, and pay special attention to normal forms resulting from combining permutative conversions and cut-elimination rules. Some of these combinations induce rewriting systems that allow for simulation of non-terminating reduction sequences known from explicit substitution calculi. Other combinations induce confluent and terminating rewriting systems whose normal forms correspond to interesting classes of terms: (i) the class of beta-normal terms of the ordinary lambda-calculus, (ii) the class of cut-free terms of Herbelin’s lambda-bar-calculus, and (iii) the class of Mints and Dyckhoff-Pinto’s normal cut-free forms. These classes are all in bijection, and reflect the existence in lambda-Jm of three alternatives to represent multiple application, i.e. application of a function to more than one argument. In the three rewriting systems, computation to normal form can be organised into two stages, so that the f irst stage consists of beta-normalisation (elimination of principal cuts) and focusing, and the second stage consists of choosing the representation of multiple application. (Joint work with José Espírito Santo and Maria João Frade.)
10:30 – 11:00	Break
11:00 – 12:30	Christian Urban	Formalising Regular Language Theory with Regular Expressions Only There are numerous textbooks on regular languages. Nearly all of them introduce the subject by describing finite automata and only mentioning on the side a connection with regular expressions. Unfortunately, automata are difficult to formalise theorem provers. The reason is that they need to be represented as graphs, matrices or functions, none of which are inductive datatypes. Also convenient operations for disjoint unions of graphs, matrices and functions are not easily formalisiable. In contrast, regular expressions can be defined conveniently as a datatype and a corresponding reasoning infrastructure comes for free. I will show in this talk that a central result from formal language theory - the Myhill-Nerode Theorem - can be recreated using only regular expressions. From this theorem many closure properties of regular languages follow.
	William Stirton	Polymorphically typed combinatory logic At present, so far as I know, no such thing as a polymorphically typed combinatory calculus exists in print. Indeed, because of the quantified types, the task of formulating one which is equivalent to the familiar polymorphically typed lambda calculus is non-trivial. I will formulate a polymorphically typed combinatory calculus and prove that it is "equivalent" to the familiar polymorphically typed lambda calculus in a sense of "equivalent" that will be defined. This calculus is of interest, of course, only in so far as it facilitates the proving of interesting metatheoretical results. I will review some of the proof-theoretical results that exist relating to the polymorphically typed lambda calculus, by Leivant, Coquand, Altenkirch and Aehlig. Special emphasis will be placed upon the fact that there is a subsystem of the calculus just strong enough to represent the primitive recursive functionals of finite type. There is at least one important question relating to this subsystem - how many contractions are needed to normalize a term? - to which no published answer has yet been given. Although it will not be possible to present my solution in detail, there are reasons for thinking that it is much easier to answer this question in relation to the combinatory calculus than in relation to the lambda calculus (by direct methods at least). Some of the foregoing has been submitted to the Archive for Mathematical Logic (and the referees recommended revisions and resubmission); but the proof of equivalence mentioned in the first paragraph above is new.
	Natasha Alechina	The logic of joint action This talk is about expressing coalitional ability (as in Coalition Logic CL) in a PDL-like logic with intersection of modalities. To be precise, we study multi-modal $K$ with intersection of modalities, interpreted over models corresponding to game structures, and give a complete axiomatisation as well as a characterisation of key complexity problems. This is joint work with Thomas Agotnes.
12:30 – 14:00	Lunch
14:00 – 15:00	Sara Negri	The geometry of proof analysis: From rule systems to systems of rules In the program of proof analysis, what are called geometric implications in categorical logic are converted into sequent calculus rules with eigenvariable conditions. This method makes it possible to convert into rules e.g. existence axioms. A generalization is proposed into a situation with several rules with eigenvariables, applied in a specific succession. The corresponding class of axioms arose from a concrete situation of proof analysis met in epistemic logic.
	Stephen Read	On GE-harmony Michael Dummett introduced the notion of harmony in response to Arthur Prior's tonkish attack on the idea of proof-theoretic justification of logical laws (or analytic validity). But Dummett vacillated between different conceptions of harmony, in an attempt to use the idea to underpin his anti-realism. Dag Prawitz had already articulated an idea of Gerhard Gentzen's into a procedure whereby elimination-rules are in some sense functions of the corresponding introduction-rules. Roy Dyckhoff, in a joint paper with Nissim Francez, `A note on harmony', finally published this year, coined the term ''general-elimination harmony'' for the relationship created by this procedure. In this talk I want to open up for discussion ways in which Roy's and my own conception of GE-harmony to some extent differ.
15:00 – 15:30	Break
15:30 – 16:30	Peter Schroeder-Heister	Proof-theoretic semantics, self-contradition, and the format of deductive reasoning From the point of view of proof-theoretic semantics, I argue that the sequent calculus with introduction rules both on the assertion and on the assumption side represents deductive reasoning more appropriately than natural deduction. In taking consequence to be conceptually prior to truth, it can deal with non-well-founded phenomena such as contradictory reasoning. The fact that in its typed variant, the sequent calculus has an explicit and separable substitution schema in form of the cut rule, is seen as a crucial advantage over natural deduction, where substitution is built into the general framework.
	Rob Rothenberg	On Labelled Sequents and Hypersequents It is part of the folklore of hypersequent calculi that they are equivalent to labelled calculi. We give an overview of recent work on the translation of proofs between formalisms that labelled calculi with relations are more expressive, meaning that there is no 1-1 translation. However, we do show that some proofs in labelled calculi can be translated into hypersequent calculi for logics with linearity.
19:00 – ...	For those who are still here, dinner together