[Prev][Next][Index][Thread]

School of Logic and COmputation program and call for participation

	School of Logic and Computation (L&C '99)
	Heriot-Watt (Edinburgh), April 10-13, 1999
	http://www.cee.hw.ac.uk/~fairouz/eefschool.html

Abstracts of the lectures can be found at
http://www.cee.hw.ac.uk/~fairouz/abstracts2.html

Abstracts of the workshops can be found at
http://www.cee.hw.ac.uk/~fairouz/abstracts2work.html

		Preliminary Schedule
	http://www.cee.hw.ac.uk/~fairouz/eefprogram.html

		Saturday, 10 April 1999

12.00 - 14.00 REGISTRATION

REWRITING WORKSHOP
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 - 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 Iteration 2-categories and Rational Term Rewriting
		Andrea Carradini and Fabio Gadducci


		Sunday, 11 April 1999

Morning Session 

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

TYPES WORKSHOP

14.00 - 14.30 Inductive and Co-Inductive Types 
		Hermans 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 - 16.30 Abstract Syntax and Variable Binding 
Marcelo Fiore, Gordon Plotkin and Daniele Turi
17.30 - 17.00 Realisability Models over linear algebras and the full 
		completeness problem for typed lambda calculi
		Marina Lenisa
17.00 - 17.30 Undecidability of second-order unification
		Jordi Levy and Margus Veanes
19:30 SOCIAL BANQUET


		Monday, 12 April 1999
Morning Session 

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 Abramski

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

12.30-14.00 LUNCH


PROOFS WORKSHOP

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 - 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  


		Tuesday, 13 April 1999

Morning Session 

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 
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

16:00 End of L&C'99