The notion of a type setup is yet one more such notion, which differs from the others in its explicit use of contexts, as finite lists of typed variable declarations. This makes it closer to the syntax of dependent type theories, while still abstracting away from the usual inductive structure of syntax and the corresponding recursive definition of substitution.

Predicate logic over a type setup is simply defined as a sorted predicate logic where the sorts are the types of the type setup and the sorted terms and substitution are also given by the type setup. Logic over a type setup generalises logic-enriched type theory which, in turn generalises dependently sorted logic, a dependent generalisation of many-sorted logic.

Many results of predicate logic generalise to predicate logic over a type setup. I will consider the disjunction and existence properties of intuitionistic predicate logic and end with a characterisation of the logic of the propositions-as-types interpretation of intuitionistic predicate logic.

My question is: How does Type Theory with continuity look like? I have some ideas but I am looking for further input (hence this seems to be a good topic for a workshop talk). It seems to me that there is a game-theoretic justification of continuity but maybe this has been studied already.

The material on the partiality monad is based on yet unpublished work with Tarmo Uustalu and Venanzio Capretta and closely related to Venanzio's paper "General Recursion via Coinductive Types".

Thanks to atomic flows, we can prove, for propositional logic, a new and very general normalisation theorem, which contains cut elimination as a special case. We also can prove cut elimination and Craig interpolation theorems, with very simple and novel constructions.

Atomic flows are much simpler objects than derivations and we can reason on them by geometric and topological methods. However, contrary to proof nets, their size is polynomially related to the size of the derivations that they represent. This allows us to employ atomic flows in proof complexity investigations.

We argue that atomic flows are a significant technical advance for normalisation theory, because 1) the technique they support is largely independent of syntax; 2) indeed, it is largely independent of logical inference rules; 3) they constitute a powerful geometric formalism, which is more intuitive than syntax.

Part of this talk is based on the paper 'Normalisation Control in Deep Inference via Atomic Flows', to appear on Logical Methods in Computer Science.

There is a deep inference overview at this webpage.

I'll give some examples of these things, and sketch some of their nice closure properties, particularly that they form a (large) Br-algebra.

A new type-theoretic framework LTT is presented and its use in formalisation and verification explained. The features of the LTT framework include:

- LTT supports practical formal reasoning with different logical foundations (“foundational pluralism”) and establishes the basis for wider applications of the type theory based theorem proving technology.
- LTT employs a notion of “typed set”, combining the type-theoretical reasoning with the set-theoretical reasoning effectively

We first propose a generalization of the notion of neutral term in Girard's candidates which allows to define candidates in a generic way. Concerning stability by union, we recall that there are confluent typed rewrite systems that do not admit stable by union type interpretations. We present a necessary and sufficient condition for Girard's candidate to be stable by union and a necessary and sufficient condition for the closure by union of biorthogonals to be reduciblity candidates. The second condition is strictly more general than the first one, and allows to define Tait's saturated sets for rewriting in a uniform way. Moreover, we show that for orthogonal constructor rewriting, Girard's candidates are stable by union.

The result of an automatic conversion of this document to pdf can be found here

Anton Setzer Last modified: Tue Apr 15 20:07:21 BST 2008