EEF Trends School in Logic and Computation

EEF Trends School of Logic and Computation (L&C '99)

Heriot-Watt (Edinburgh), April 10-13, 1999

http://www.cedar-forest.org/forest/events/eefschool1999/eefschool.html

ULTRA logo ULTRA group
Useful Logics, Types, Rewriting,
and Applications UKII
UK Institute of Informatics,
UK

Preliminary Schedule

http://www.cedar-forest.org/forest/events/eefschool1999/eefprogram.html

Saturday, 10 April 1999

12.00 - 14.00 REGISTRATION

TYPES WORKSHOP

14.00 - 15.30 Chair: Ian Stark

14.00 - 14.30 Inductive and Co-Inductive Types
Herman Geuvers

14.30 - 15.00 Names, Binding and Substitution
Randy Pollack

15.00 - 15.30 A Type Theory for Classical Arithmetic
Charles Stewart

15.30 - 16.00 BREAK

16.00 - 17.30 Chair: Herman Geuvers

16.00 - 16.30 Iteration 2-categories and Rational Term Rewriting
Andrea Corradini and Fabio Gadducci

16.30 - 17.00 Realisability Models over linear combinatory algebras and the full completeness problem for typed lambda calculi
Samson Abramsky and Marina Lenisa

17.00 - 17.30 Undecidability of second-order unification
Jordi Levy and Margus Veanes

Sunday, 11 April 1999

Morning Session Chair: Joe Wells

9.00 - 10.00 The Expressive Power of Higher-order Types or, Life without CONS
Neil Jones

10.00 - 10.30 BREAK

10.30 - 11.30 Theorem Proving Modulo
Claude Kirchner

11.30 - 12.30 Some New Developments in Unification Related to Type Theory
Assaf Kfoury

     12.30 - 14.00        LUNCH

REWRITING WORKSHOP

14.00 - 15.30 Chair: Jos Baeten

14.00 - 14.30 Rewriting with extensionality
Roberto Di Cosmo

14.30 - 15.00 Extending Partial Combinatory Algebras
Inge Bethke, Jan Willem Klop and Roel de Vrijer

15.00 - 15.30 Higher-Order Rewriting
Femke van Raamsdonk

15.30 - 16.00 BREAK

16.00 - 18.00 Chair: Jan-Willem Klop

16.00 - 16.30 Meaningless Terms in Rewriting
Richard Kennaway, Vincent van Oostrom and Fer-Jan de Vries

16.30 - 17.00 A Geometric Proof of Confluence by Decreasing Diagrams
Jan Willem Klop, Roel de Vrijer and Vincent van Oostrom

17.00 - 17.30 Pi calculus in Co-inductive Type Theory
Furio Honsell, Marino Miculan and Ivan Scagnetto

17.30 - 18.00 Modeling binary methods: Some problems and results
Hendrik Tews

Monday, 12 April 1999

Morning Session Chair: Achim Jung

9.00 - 10.00 Applications of Classes and Types to Practical Verifications
Robert Constable

10.00 - 10.30 BREAK

10.30 - 11.30 Concurrent Games and Full Completeness for Linear Logic
Samson Abramsky

11.30 - 12.30 The Lambda Calculus in Different Scenarios
Mariangola Dezani-Ciancaglini

     12.30 - 14.00        LUNCH

PROOFS WORKSHOP

14.00 - 15.30 Chair: Didier Galmiche

14.00 - 14.30 Proof Search issues in constructive logic
Roy Dyckhoff

14.30 - 15.00 Truth as Simulation: Towards a Co-algebraic perspective on logic and games.
Alexandru Baltag

15.00 - 15.30 Decidability of context unification
Jordi Levy and Mateu Villaret

15.30 - 16.00 BREAK

16.00 - 18.00 Chair: Roy Dyckhoff

16.00 - 16.30 Some Issues about Proof Search in Linear Logic
Didier Galmiche

16.30 - 17.00 Lambda Terms for natural deduction, sequent calculus and cut elimination
Henk Barendregt and Sylvia Ghilezan

17.00 - 17.30 Revisiting Kreisel: A Computational Anomaly in the Troelstra-Schwichtenberg G3i system
Rene Vestergaard

17.30 - 18.00 Theorema: Overview on using the system
Wolfgang Windsteiger

                       19.30         SOCIAL BANQUET

Tuesday, 13 April 1999

Morning Session Chair: Don Sannella

9.00 - 10.00 The Curry-Howard Isomorphism: Remarks on Recursive Types
Pawel Urzyczyn

10.00 - 10.30 BREAK

10.30 - 11.30 A New Approach to Abstract Syntax Involving Binders
Andrew Pitts

11.30 - 12.30 Origin Tracking in Term Rewriting
Jan Willem Klop

     12.30 - 14.00        LUNCH

Afternoon Session Chair: Fairouz Kamareddine

14.00 - 15.00 The Mathematical Universe according to Brouwer
Dirk van Dalen

15.00 - 15.30 BREAK

15.30 - 16.30 Mission possible: proof-checking
Henk Barendregt

16.30 - 17.30 What is the logical strength of the Lego and Coq Type Theories?
Peter Aczel

                       18.00          END of L&C'99

Lectures abstracts can be found at: http://www.cedar-forest.org/forest/events/eefschool1999/abstracts2.html
Workshops abstracts can be found at: http://www.cedar-forest.org/forest/events/eefschool1999/abstracts2work.html
Travel information can be found at: http://www.cedar-forest.org/forest/events/eefschool1999/eeftravel.html

14.00 - 15.30	Chair: Ian Stark
14.00 - 14.30	Inductive and Co-Inductive Types Herman Geuvers
14.30 - 15.00	Names, Binding and Substitution Randy Pollack
15.00 - 15.30	A Type Theory for Classical Arithmetic Charles Stewart
15.30 - 16.00	BREAK
16.00 - 17.30	Chair: Herman Geuvers
16.00 - 16.30	Iteration 2-categories and Rational Term Rewriting Andrea Corradini and Fabio Gadducci
16.30 - 17.00	Realisability Models over linear combinatory algebras and the full completeness problem for typed lambda calculi Samson Abramsky and Marina Lenisa
17.00 - 17.30	Undecidability of second-order unification Jordi Levy and Margus Veanes

9.00 - 10.00	The Expressive Power of Higher-order Types or, Life without CONS Neil Jones
10.00 - 10.30	BREAK
10.30 - 11.30	Theorem Proving Modulo Claude Kirchner
11.30 - 12.30	Some New Developments in Unification Related to Type Theory Assaf Kfoury

14.00 - 15.30	Chair: Jos Baeten
14.00 - 14.30	Rewriting with extensionality Roberto Di Cosmo
14.30 - 15.00	Extending Partial Combinatory Algebras Inge Bethke, Jan Willem Klop and Roel de Vrijer
15.00 - 15.30	Higher-Order Rewriting Femke van Raamsdonk
15.30 - 16.00	BREAK
16.00 - 18.00	Chair: Jan-Willem Klop
16.00 - 16.30	Meaningless Terms in Rewriting Richard Kennaway, Vincent van Oostrom and Fer-Jan de Vries
16.30 - 17.00	A Geometric Proof of Confluence by Decreasing Diagrams Jan Willem Klop, Roel de Vrijer and Vincent van Oostrom
17.00 - 17.30	Pi calculus in Co-inductive Type Theory Furio Honsell, Marino Miculan and Ivan Scagnetto
17.30 - 18.00	Modeling binary methods: Some problems and results Hendrik Tews

9.00 - 10.00	Applications of Classes and Types to Practical Verifications Robert Constable
10.00 - 10.30	BREAK
10.30 - 11.30	Concurrent Games and Full Completeness for Linear Logic Samson Abramsky
11.30 - 12.30	The Lambda Calculus in Different Scenarios Mariangola Dezani-Ciancaglini

14.00 - 15.30	Chair: Didier Galmiche
14.00 - 14.30	Proof Search issues in constructive logic Roy Dyckhoff
14.30 - 15.00	Truth as Simulation: Towards a Co-algebraic perspective on logic and games. Alexandru Baltag
15.00 - 15.30	Decidability of context unification Jordi Levy and Mateu Villaret
15.30 - 16.00	BREAK
16.00 - 18.00	Chair: Roy Dyckhoff
16.00 - 16.30	Some Issues about Proof Search in Linear Logic Didier Galmiche
16.30 - 17.00	Lambda Terms for natural deduction, sequent calculus and cut elimination Henk Barendregt and Sylvia Ghilezan
17.00 - 17.30	Revisiting Kreisel: A Computational Anomaly in the Troelstra-Schwichtenberg G3i system Rene Vestergaard
17.30 - 18.00	Theorema: Overview on using the system Wolfgang Windsteiger

9.00 - 10.00	The Curry-Howard Isomorphism: Remarks on Recursive Types Pawel Urzyczyn
10.00 - 10.30	BREAK
10.30 - 11.30	A New Approach to Abstract Syntax Involving Binders Andrew Pitts
11.30 - 12.30	Origin Tracking in Term Rewriting Jan Willem Klop

14.00 - 15.00	The Mathematical Universe according to Brouwer Dirk van Dalen
15.00 - 15.30	BREAK
15.30 - 16.30	Mission possible: proof-checking Henk Barendregt
16.30 - 17.30	What is the logical strength of the Lego and Coq Type Theories? Peter Aczel