10:00 – 10:15 
Welcome 

10:15 – 11:15 
Jamie Gabbay 
Prooftheory for metaprogramming and modal type theory Calculi based on intuitionistic S4 are a basis for certain kinds of metaprogramming, 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. 
Didier Galmiche 
Labelfree 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 multicontextual structure, called Tsequent, 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 subformula property
in the intuitionistic case. 

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 cutfree 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 agentindexed 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.


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 humancomputer dialogues A dialogue is seen as the refinement of a mathematical object. The syntactic wellformedness 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.

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 cutfree derivations, and not much attention is paid to the interaction between cutelimination and permutative conversions. Nonetheless, the class of cutfree derivations is known to exhibit redundancies, when mapped into natural deduction. In particular, Mints and DyckhoffPinto, independently, identified a class of “normal cutfree” derivations in bijection with normal natural deductions, which arises as the class of normal forms w.r.t. certain permutative conversions.


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 MyhillNerode 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 nontrivial. 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.


Natasha Alechina 
This talk is about expressing coalitional ability (as in Coalition Logic CL) in a PDLlike logic with intersection of modalities. To be precise, we study multimodal $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 
Michael Dummett introduced the notion of harmony in response to Arthur Prior's tonkish attack on the idea of prooftheoretic 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 antirealism. Dag Prawitz had already articulated an idea of Gerhard Gentzen's into a procedure whereby eliminationrules are in some sense functions of the corresponding introductionrules. Roy Dyckhoff, in a joint paper with Nissim Francez, `A note on harmony', finally published this year, coined the term ''generalelimination 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 GEharmony to some extent differ. 

15:00 – 15:30 
Break 

15:30 – 16:30 
Peter SchroederHeister 
Prooftheoretic semantics, selfcontradition, and the format of deductive reasoning From the point of view of prooftheoretic 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 nonwellfounded 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 11 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 