Lorentz Center - Mathematics: Algorithms and Proofs from 8 Jan 2007 through 12 Jan 2007
  Current Workshop  |   Overview   Back  |   Home   |   Search   |     

    Mathematics: Algorithms and Proofs
    from 8 Jan 2007 through 12 Jan 2007

 
Program Mathematics: Algorithms and Proofs

Program Mathematics: Algorithms and Proofs

 

All talks include 5 minutes for questions

 

Monday, 8 January

 

09:00-09:25        Registration and Coffee

09:20-09:25        Introduction by Mrs. Martje Kruk-de Bruin (Lorentz Center)

09:25-09:30        Opening of the workshop by Bas Spitters

 

09:30-10:30        Lenstra

 

Coffee/Tea break

 

10:50-11:35        Cohen

11:40-12:25        Cohen

 

Lunch break

 

14:40-15:40        O’Connor

                             Spitters

 

Coffee/Tea break

 

16:00-17:00        Romero Ibañez

                             Aransay

 

17:00                   Wine and Cheese party (Common Room Lorentz Center)

 


 

Tuesday, 9 January

 

09:00-10:00        Paule

 

Coffee/Tea break

 

10:25-11:10        Martin-Löf

11:15-12:00        Martin-Löf

 

Lunch break

 

14:40-15:40        Mahboubi

                             McLaughlin

 

Coffee/Tea break

 

16:00-17:00        Passmore

                             Draisma

 

Evening:               Business Meeting

 

 

 

 

Wedneday, 10 January

 

09:00-10:00        Edwards

 

Coffe/Tea break

 

10:25-11:10        Coquand

11:15-12:00        Coquand

 

Lunch break

 

14:30                             Excursion

                             Followed by conference dinner on a boat

 


Thursday, 11 January

 

09:00-10:00        Beeson

 

Coffee/Tea Break

 

10:25-11:10        Martin-Löf

11:15-12:00        Martin-Löf

 

Lunch break

 

14:10-15:40        Dowek

                             Oliva

                             Briseid

 

Coffee/Tea break

 

16:00-17:00        De Smit: Escher and the Droste Effect

 

 

Friday, 12 January

 

09:00-10:00        Lombardi

 

Coffee/Tea break

 

10:20-11:20        Van Dalen

11:25-12:10        Cohen

 

Lunch break

 

13:00-14:00        Hancock

                             Altenkirch

 

Coffee/Tea break

 

14:20-15:20        Schwichtenberg

                             Schuster

 

15:20-15:25        Closing     

Tutorials:

 

Arjeh Cohen (Technische Universiteit Eindhoven)

Three aspects of exact computation

 

Thierry Coquand (Chalmers)

A logical approach to abstract algebra

 

Per Martin-Löf (Stockholm)

Topos Theory and Type Theory

 

 

Invited talks:

 

Michael Beeson

Algorithms and Proofs in Geometry

 

Dirk van Dalen (Utrecht University)

The lonely revolutionary. Brouwer’s first program

 

Hendrik Lenstra (Universiteit Leiden)

Ordering fields

 

 

Contributed talks:

 

Thorsten Altenkirch (Nottingham)

Quotient Types in Observational Type Theory

 

Jesus Aransay (La Rioja)

A mechanised proof of the Basic Perturbation Lemma

 

Eyvind Briseid (Darmstadt)

Using proof mining to find computable rates of convergence for the Picard iteration sequence for non-nonexpansive functions

 

Jan Draisma (Technische Universiteit Eindhoven)

A scenic tour in tropical geometry

 

Gilles Dowek (l’École polytechnique)

The linear-algebraic lambda-calculus (joint work with Pablo Arrighi)

 

Harold Edwards (New York)

Addition on Elliptic Curves


 

Peter Hancock (Edinburgh)

Stream Processing, a la Brouwer (Joint work with Neil Ghani and Dirk Pattinson)

 

Assia Mahboubi (INRIA/MSR)

A formal correctness proof for the subresultant algorithm

 

Sean McLaughlin (CMU)

A Methodology for Implementing Reusable Decision Procedures

 

Henri Lombardi (France Comté)

Constructive real algebra

 

Russell O’Connor (Radboud University)

Implementing Analysis

 

Paulo Oliva (Queen Mary, University of London)

Modified realizability of classical linear logic

 

Grant Olney Passmore (University of Texas, Austin)

Mechanized Theory Development for Formal Computation and Proof in Elementary Algebraic Theories with Small Models

 

Peter Paule (Research Institute for Symbolic Computation (RISC), J. Kepler University Linz, Austria)

A Computer Proof of a Conjecture of Moll

 

Ana Romero Ibañez (Rioja)

Constructive Spectral Sequences

 

Peter Schuster (Munich)

Labelled Trees of Finite Depth (joint work with Hervé Perdry)

 

Helmut Schwichtenberg (Munich)

Goedels Dialectica Interpretation

 

Bas Spitters (Radboud University)

Located and overt locales (jww Thierry Coquand)



   [Back]