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



Coffee/Tea break


16:00-17:00        Romero Ibañez



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



Coffee/Tea break


16:00-17:00        Passmore



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




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



Coffee/Tea break


14:20-15:20        Schwichtenberg



15:20-15:25        Closing     



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)