Invited Speakers

List of confirmed invited speakers and tutorials:

    • Nachum Dershowitz

Title: Turing Centenary Lectures

Abstract: This tutorial will describe the fundamental work of Alan Turing in the fields of Logic, Mathematics and Computer Science and its consequences. In particular:

    1. A proof of the Church-Turing thesis: We will look at the history of the Church-Turing thesis, which states that every effectively computable function is computable in the Turing sense. An axiomatizing of effective computation allows to proof the thesis.

    2. Beyond the Church-Turing thesis: We will present arguments for and against hyper-computation, the notion that human beings or structures can compute non-computable functions (in the Turing sense).

    3. An extension to the Church-Turing thesis: We will show an extended Church-Turing thesis in the sense that every effective algorithm can be simulated in an effective way by a Turing Machine. In fact, such algorithm is generated by an abstract state machine, which is simulated by a machine of random access with a linear overhead.

    • Maribel Fernández

Title: Nominal Techniques

Abstract: Nominal logic is a generalization of first-order logic that allows us to deal with syntax involving binding operators in an elegant and practical way. Nominal systems maintain a strict distinction between atoms (variables that may be bound by a special abstraction operation) and meta-variables (or just variables) which cannot be bound, giving the framework a pronounced first-order character since substitution is not capture-avoiding. In nominal syntax, bound entities are explicitly named (rather than using a nameless syntax such as de Bruijn indices), yet we get a formalism that respects alpha-equivalence and can be directly implemented. Nominal unification is decidable (unlike higher-order unification), and efficient unification algorithms are available. Nominal rewriting can be seen as a form of higher-order rewriting with a first-order syntax and built-in alpha-equivalence.

In these lectures, we will introduce the nominal approach to the specification of systems with binding operators, and we will show how good properties of first-order rewriting are inherited by the nominal rewriting framework. We will describe an efficient matching algorithm that has been used to implement a nominal rewriting tool.

    • Pedro Quaresma

Title: Geometric Theorem Provers

Abstract: Proving geometric theorems has been an interesting challenge is automatic theorem provers, ever since the seminal works from Gelernter in 1959 an others, until the current provers based on algebraic methods (Wu 2000, Wang 1995, Kapur 1986, Li 2000) and semi-algebraic (Chou 1996). A particularly important issue is proving theorems that require additional elements to the original construction.

In this tutorial we will present the journey taken by Geometric Automated Theorem Provers (GATP) from the axiomatic systems (that although having the advantage of working over axiomatic geometric systems and producing geometric proofs, are in general very restrictive in the type of geometric construction one can consider) to the algebraic systems. In between we will consider mixed systems, such as the area method, probabilistic proof, among others.

We will also present some of the current challenges of GATPs, in particular concerning the formalization of geometric systems, the iterative and interactive proof of theorems, the generation of proofs understood by geometers and visual proofs and the integration with systems of dynamic geometry.

    • Guy Wallet

Title: Nonstandard Type Theory

Abstract: The aim of these lectures is to introduce to Per Martin-Löf's ideas about a constructive approach of Nonstandard Analysis using the intuitionistic concept of choice sequence reconsidered within Constructive Type Theory. For the first time, these ideas appeared in the article Mathematics of Infinity published in 1989. Although he has published nothing more on this topic, Martin-Löf never stopped his research toward a general Nonstandard Type Theory. Following some recent discussions with him, a more elaborate version of this theory is going to emerge.

These lectures will give the state of the art on this subject.