SEMINARS/SCHOOLS/EVENTS 2000-2001

June 2001 1 June 2001 ULTRA room 233 Type Theories from Barendregt's Cube for Theorem Provers. Here are slides Jonathan Seldin, Lethbridge University, Canada 1 June 2001 ULTRA room 233 Curry's Last Problem, Imitating Lambda-beta-reduction in Combinatory Logic Roger Hindley, University of Swansea, UK December 2000 5 Dec 2000 ULTRA HLTR'00 Workshop on History of Logics, Types and Rewriting(HLTR '00) ULTRA, Heriot-Watt University 5 December 2000 ULTRA HLTR'00 Quine's New Foundations (NF) Carsten Butz, Heriot-Watt University, UK 5 December 2000 ULTRA HLTR'00 Birth of Lambda calculus and combinatory logic Roger Hindley, University of Swansea, UK 5 December 2000 ULTRA HLTR'00 Mathematics and symbolic logics: an uneasy relationship of the 20th century Ivor Grattan-Guinness, Middlesex University, UK 5 December 2000 ULTRA HLTR'00 History of Types in Logic and Mathematics Fairouz Kamareddine, Heriot-Watt University, UK

SEMINARS/SCHOOLS/EVENTS 1999-2000

July 2000 16-18 July 2000 ULTRA FC '00 Workshop on Foundations and Computations(FC'00) Fairouz Kamareddine, Heriot-Watt University 16 July 2000 ULTRA FC '00 Aircraft Trajectory Modeling and Analysis: A challenge to Formal Methods Cesar Munoz, ICASE, NASA, USA 16 July 2000 ULTRA FC '00 Compositional Characterizations of lambda terms using intersection types Yoko Motohama, Torino University, Italy 16 July 2000 ULTRA FC '00 A programming approach to descriptive complexity theory Iain Stewart, University of Leicester, UK 16 July 2000 ULTRA FC '00 A Weak Constructive Set Theory witsh Inaccessible sets Laura Crosilla, Leeds, UK 17 July 2000 ULTRA FC '00 Correspondences between Classical, Intuitionistic and Uniform Provability and their Impact on Proof Search Gopalan Nadathur, University of Chicago, USA 17 July 2000 ULTRA FC '00 Automating Newton's calculus in Isabelle Jacques Fleuriot, University of Edinburgh, UK 17 July 2000 ULTRA FC '00 Dynamic First Order Logic Jan van Eijck, University of Amsterdam, NL 17 July 2000 ULTRA FC '00 The calculus of contexts of lambda-sigma Therese Hardin, Paris 6 and INRIA-Rocquencourt, France 17 July 2000 ULTRA FC '00 The Brisk machine: the next step in the execution of functional languages Eleni Spiliopoulou, Bristol, UK 17 July 2000 ULTRA FC '00 Type Based Decompilation Alan Mycroft, Cambridge University and AT&T Labs, UK 17 July 2000 ULTRA FC '00 Gaurded Exception Handling: Some results Catherine Piliere, INRIA, FR 18 July 2000 ULTRA FC '00 The birth of lambda-calculus and combinatory logic Roger Hindley, Swansea, UK 18 July 2000 ULTRA FC '00 About Folding-Unfolding Cuts Gilles Dowek, Inria, Rocquencourt, France 18 July 2000 ULTRA FC '00 Extensional Set Equality in the Calculus of Constructions Jonathan Seldin, Lethbridge, Canada 18 July 2000 ULTRA FC '00 Formal languages applied to group theory Sarah Rees, Newcastle, UK 18 July 2000 ULTRA FC '00 A Tableaux system for a fragment of the hyperset theory Massimo Felici 15 July 2000 Joe Wells ICALP '00 Geneva Workshop on Intersection Types and Related Systems (ITRS '00) Joe Wells, Heriot-Watt University 7 July 2000 3.15 pm ULTRA room 170 On Interreduction of Semi-Complete Rewrite Systems Bernhard Gramlich, Vienna University of Technology June 2000 28 June 2000 3.15 pm ULTRA room 170 Strategies for Higher Order Unification in Explicit Substitutions. Here are the slides of the talk. Mauricio Ayala Rincon, Brasilia University. May 2000 7 June 2000 3.15 pm ULTRA room 170 Equational Reasoning for Linking with First-Class Primitive Modules Joe Wells, Heriot-Watt University 8 May 2000 3.15 pm ULTRA room 170 Deciding Isomorphisms of Simple Types in Polynomial Time Jeff Considine, Boston University April 2000 6-16 April 2000 ULTRA room 2.44 The School in Deduction and Theorem Proving'00. Fairouz Kamareddine, Heriot-Watt University 6 April 2000 ULTRA DTP'00. Tutorial on Proof General David Aspinall, Edinburgh University, UK 6 April 2000 ULTRA DTP'00. tutorial on dependently typed records for representing mathematical structure Randy Pollack, Edinburgh University, UK 7 April 2000 ULTRA DTP'00. 2 lectures on Algorithmic Proof Nicola Olivetti, University of Turin, Italy 7 April 2000 ULTRA DTP'00. tutorial on Algorithmic Proof Nicola Olivetti, University of Turin, Italy 7 April 2000 ULTRA DTP'00. lecture on Explicit Substitutions in (Typed) Lambda Calculi Fairouz Kamareddine, Heriot-Watt university, UK 7 April 2000 ULTRA DTP'00. lecture on syntax for implicit text in formal proofs Stefano Berardi, University of Turin, Italy 7 April 2000 ULTRA DTP'00. tutorial on syntax for implicit text in formal proofs Stefano Berardi, University of Turin, Italy 8 April 2000 ULTRA DTP'00. lecture on Algorithmic Proof Nicola Olivetti, University of Turin, Italy 8 April 2000 ULTRA DTP'00. tutorial on Algorithmic Proof Nicola Olivetti, University of Turin, Italy 8 April 2000 ULTRA DTP'00. tutorial on Theorem Proving and Programming with Dynamic First Order Logic Jan van Eijck, University of Amsterdam, NL 8 April 2000 ULTRA DTP'00. lecture on syntax for implicit text in formal proofs Stefano Berardi, University of Turin, Italy 8 April 2000 ULTRA DTP'00. tutorial on syntax for implicit text in formal proofs Stefano Berardi, University of Turin, Italy 10 April 2000 ULTRA DTP'00. lecture on Intersection types: Syntax and Semantics Mariangiola Dezani, University of Turin, Italy 10 April 2000 ULTRA DTP'00. 3 lectures on The Automath System for Verification of Mathematics N.G. de Bruijn, Eindhoven, NL 10 April 2000 ULTRA DTP'00. lecture on Types and Properties of Lambda Terms Mariangiola Dezani, University of Turin, Italy 10 April 2000 ULTRA DTP'00. lecture on Explicit Reductions and Definitions in (Typed) Lambda Calculi Fairouz Kamareddine, Heriot-Watt University, UK 11 April 2000 ULTRA DTP'00. lecture on Types and Lambda Trees Mariangiola Dezani, University of Turin, Italy 11 April 2000 ULTRA DTP'00. tutorial on The Automath System for Verification of Math N.G. de Bruijn, Eindhoven, NL 11 April 2000 ULTRA DTP'00. lecture on Algorithmic Proof Nicola Olivetti, University of Turin, Italy 11 April 2000 ULTRA DTP'00. 2 lectures on Isabelle and Designing a Theorem Prover Larry Paulson, University of Cambridge, UK 11 April 2000 ULTRA DTP'00. tutorials and practicals on Isabelle Jacques Fleuriot, University of Edinburgh, UK 12 April 2000 ULTRA DTP'00. 2 lecture on Isabelle and Designing a Theorem Prover Larry Paulson, University of Cambridge, UK 12 April 2000 ULTRA DTP'00. practicals and tutorials on Isabelle and Designing a Theorem Prover Jacques Fleuriot, University of Edinburgh, UK 13 April 2000 ULTRA DTP'00. 2 lectures on Modal and Temporal Logics Colin Stirling, University of Edinburgh, UK 13 April 2000 ULTRA DTP'00. tutorial on Modal and Temporal Logics Colin Stirling, University of Edinburgh, UK 13 April 2000 ULTRA DTP'00. 2 lectures on Types in Logic, Mathematics and Programming Robert Constable, Cornell University, USA 13 April 2000 ULTRA DTP'00. lecture on Coq Daniel Hirschkoff, INRIA and CNRS, Fr 14 April 2000 ULTRA DTP'00. 3 lectures on Coq Daniel Hirschkoff, INRIA and CNRS, Fr 14 April 2000 ULTRA DTP'00. lecture on Types in Logic, Mathematics and Programming Robert Constable, Cornell University, USA 14 April 2000 ULTRA DTP'00. practicals on Coq Daniel Hirschkoff, INRIA and CNRS, Fr 15 April 2000 ULTRA DTP'00. lecture on Algorithmic Proof Nicola Olivetti, University of Turin, Italy 15 April 2000 ULTRA DTP'00. practical on Coq Daniel Hirschkoff, INRIA and CNRS, Fr 15 April 2000 ULTRA DTP'00. 2 lectures on Computation and deductions by rewriting with ELAN Claude Kirchner, Nancy, France 15 April 2000 ULTRA DTP'00. tutorial on Computation and deductions by rewriting with ELAN Claude Kirchner, Nancy, France 16 April 2000 ULTRA DTP'00. lecture on Computation and deductions by rewriting with ELAN Claude Kirchner, Nancy, France 16 April 2000 ULTRA DTP'00. tutorial on Computation and deductions by rewriting with E Claude Kirchner, Nancy, France February 2000 1-3 February 2000 ULTRA Cedar Room Winter Workshop on Logics, Types and Rewriting'00. Fairouz Kamareddine, Heriot-Watt University December '99 Wed 1 December 16:15 ULTRA room 302 On Automating Inductive and Non-Inductive Termination Methods Francois Monin, Heriot-Watt University November'99 Wed 24 November 16:15 ULTRA room 302 A Paradigm Shift in Program Analysis and Transformation via Intersection and Union Types Joe Wells, Heriot-Watt University

SEMINARS/SCHOOLS/EVENTS 1998-1999

August'99 17 August'99 4 pm ULTRA room 2.33 Issues in the Design and Implementation of a Higher order Metalanguage Professor Gopalan Nadathur, University of Chicago. 6-11 August'99 ULTRA room 2.33 Logic of Agents and Actions event Also, see this related event by Dov Gabbay's wife, Lydia Rivlin. Professors Dov Gabbay King's college, London and John Woods, Lethbridge University, Canada. June'99 2-6 June'99 ULTRA room 2.33 Programming Language Concepts drs. Johan Agat, Chalmers University April'99 10-13 April'99 ULTRA room 2.44 The EEF Trends school in Logic and Computation Fairouz Kamareddine, Heriot-Watt University February '99 24 February'99 ULTRA room 1.80 the purpose and methods of SHEFC resaerch funding. Morag Campbell, Shefc January '99 11 January'99 ULTRA room 2.33 Type Inference for Intersection Types using Expansion Variables . Joe Wells, Heriot-Watt University November'98 2 November'98 ULTRA room 233 Flow-Based Function Representation Transformation Joe Wells, Heriot-Watt University 26 November'98 ULTRA room 127 Joint Symposium on Computational Models of Brain, Language and Reasoning Fairouz Kamareddine, Heriot-Watt University

SEMINARS/SCHOOLS/EVENTS 1997-1998

June '98 Wed 10 June 1600 Beauty F091 A stability theorem in rewriting theory Paul-Andre Mellies, University of Edinburgh May '98 Wed 27 May 1600 Beauty F091 Decidability of Higher Order Subtyping via Logical Relations Adriana Compagnoni, University of Edinburgh Wed 13 May 1600 Beauty F091 Branching and Independence Semantics of Dataflow Networks Thomas Hildebrandt, (BRICS, Aarhus) Apr '98 Wed 22 Apr 1600 Beauty F161 The Cut Rule and Explicit Substitutions Rene Vestergaard, University of Glasgow March '98 29 March RTA Japan The First International Workshop on Explicit Substitutions: Theory and Applications to Programs and Proofs: WESTAPP '98 . See also Westapp'99 and Westapp'00. Fairouz Kamareddine, Japan Wed 18 Mar 1600 Beauty F161 Coercive subtyping: a general approach to subtyping and inheritance Zhaohui Luo, University of Durham Wed 11 Mar 1600 Beauty F161 No MEETING Wed 04 Mar 1600 Beauty F161 Categorical Investigations of Abstract Syntax Marcelo Fiore, University of Edinburgh February '98 Wed 25 Feb 1600 Beauty F161 Progress on Substitutions Fairouz Kamareddine, University of Glasgow Wed 18 Feb 1600 Beauty F161 Intuitionistic Sequent Calculi Roy Dykhoff, University of St Andrews Wed 11 Feb 1600 Beauty F161 Names, Binding and Substitution Randy Pollack, University of Glasgow Mon 09 Feb 1600 Beauty conference room A Computational Interpretation of the $\lambda\mu$-calculus Gavin Bierman, University of Cambridge Wed 04 Feb 1600 Beauty 3a (Maths) Term Rewriting Prof. Stephen Pride, University of Glasgow January '98 Wed 21 Jan 1600 Beauty F161 Extending type theory to classical logic Charles Stewart, University of Oxford December '97 Wed 03 Dec 1600 Beauty F161 What are types? Open discussion led by Joe Wells, University of Glasgow November '97 Wed 26 Nov 1600 Beauty F161 The latest developments in substitution calculi in Glasgow, France and Holland. Fairouz Kamareddine, University of Glasgow Wed 19 Nov 1600 Beauty F161 An ALF proof that reductions in \s can be simulated in \sigma Qiao Haiyan, University of Glasgow Wed 12 Nov 1600 Beauty F161 A Closer Look at the Curry-Howard Correspondence: A Proof Theoretical Presentation of Reductions in \-like calculi Rene Vestergaard, University of Glasgow Wed 05 Nov 1600 Beauty F161 An Introduction to Higher-Order Rewriting Joe Wells, University of Glasgow October '97 Wed 29 Oct 1600 Beauty F161 Progress Report on Explicit Substitution Fairouz Kamareddine, University of Glasgow Wed 22 Oct 1600 Beauty F161 Introduction and Discussion

SEMINARS/SCHOOLS/EVENTS 1996-1997

April '97 Friday 25 Apr 1600 Beauty F161 The use of explicit substitutions in theorem proving Fairouz Kamareddine, University of Glasgow February '97 Friday 14 Feb 1600 Beauty F161 Introducing Beauty to Haskell Richard reid, University of Glasgow Friday 7 Feb 1600 Beauty F161 Local and Explicit Substitutions Alejandro Rios, University of Glasgow January '97 Friday 24 Jan 1600 Beauty F161 The next collaborations and papers Fairouz Kamareddine, University of Glasgow December '96 Friday 13 Dec 1600 Beauty F161 A proposed tool for working with the lambda calculus Richard reid, University of Glasgow Friday 6 Dec 1600 Beauty F161 Simply typed lambda calculus with explicit substitutions and open terms Fairouz Kamareddine, University of Glasgow November '96 Friday 29 Nov 1600 Beauty F161 How can the newly funded EPSRC project fit with our two existing ones. Fairouz Kamareddine, University of Glasgow Friday 22 Nov 1600 Beauty F161 Splitting and Typing Relation Fairouz Kamareddine, University of Glasgow Friday 15 Nov 1600 Beauty F161 Informal Discussion Beauty, University of Glasgow Friday 8 Nov 1600 Beauty F161 Alejandro Rios, University of Glasgow Friday 1 Nov 1600 Beauty F161 Explicit definitions and substitutions Fairouz Kamareddine, University of Glasgow October '96 Friday 18 Oct 1600 Beauty F161 Introduction Fairouz Kamareddine, University of Glasgow September '96 12-15 September Beauty conference room The First International School on Type Theory and Term Rewriting '96 Fairouz Kamareddine, University of Glasgow

Maintained by Fairouz Kamareddine ()