Glynn Winskel - Curriculum vitae#

Qualifications:

• B.A. in Mathematics, M.A., University of Cambridge (1975).
• M.Sc. in Mathematics, specialising in Mathematical Logic, University of Oxford (1976).
• Ph.D. in Computer Science, University of Edinburgh (Awarded 1980, Conferred 1981).
• Sc.D., University of Cambridge (1995).

Positions:

• Research Associate, Computer Science Department, University of Edinburgh (September 1979–August 1980).
• Visiting Lecturer, Computer Science Department, University of Aarhus, Denmark (September 1980–December 1980)
• Royal Society Postdoctoral Research Fellow, University of Aarhus, Denmark (January 1981–January 1982)
• Research Scientist, Computer Science Department, Carnegie-Mellon University (March 1982–December 1983)
• University Lecturer in Computer Science, University of Cambridge (January 1984–October 1987)
• Director of Studies in Computer Science at King’s College, Cambridge(October 1984–September 1985)
• Fellow of King’s College, Cambridge (July 1985–July 1988).
• Reader in Theoretical Computer Science ad hominem, University of Cambridge (October 1987–July 1988)
• Professor of Computer Science, University of Aarhus, Denmark (July 1988–October 2000)
• Director of BRICS, Centre for Basic Research in Computer Science, University of Aarhus, Denmark (January 1994–October 2000)
• Professor of Computer Science, University of Cambridge, England (October 2000–).
• Fellow of Emmanuel College, Cambridge (October 2000–).

Consultancy:

• TopExpress, Cambridge (1986–87).
• Microsoft Research Laboratory, Cambridge, Visiting Researcher (around 2 months a year) (1998–2000)

Research interests:

Theoretical computer science and related mathematics, especially applications of logic and category theory to computer science. Interests range through the semantics of programming languages, mathematical foundations of denotational semantics, domain theory, logic of programs, mathematical models and proof systems for concurrent computation, models and proof systems for the specification and verification of hardware, type theories, functional programming, automated proof, model checking, computer security. Administration: Sundry university and college committees. Aarhus: Director of BRICS (1994-2000). Cambridge: Chair of Senior Promotions, Director of Graduate Education, On committee for internal review of Mathematics at Cambridge (2004), Head of Emmanuel College Research Fellowships Committee (2005-6), (2008-9).

Miscellaneous activities:

On the editorial board of “Mathematical Structures in Computer Science” Cambridge University Press. On the editorial board of “Transactions on Petri Nets and Other Models of Concurrency” Springer Lecture Notes in Computer Science. Guest Editor of Information and Computation LICS’97 Special Issue. Guest Editor “Annals of Pure and Applied Logic” devoted to the proceedings of PTAC (1998). Member of LICS Organizing Committee (1996–2003), Advisory Committee (2004–), on the three-man LICS Testof- Time Award Committee 2006-7 and 2008-9, Chair of LICS Test-of-Time Award Committee 2009-2010. Advisory board of the journal Higher-Order and Symbolic Computation. Editorial Board of Semantic Structures in Computation, Kluwer Academic Publishers. Advisory Board Higher Order and Symbolic Computation (HOSC) (2002—). On Board of EASL (European Association of Symbolic Logic) (2005—). Served as referee for numerous international journals and conferences as well as reviewer of NSF and Canadian research proposals. I organised the BRICS Summer School in Semantics of Computation, 1999. Served on numerous evaluation committees, occasionally as chairman. Some programme committees: Mathematical Foundations of Program Semantics, New Orleans, 1995; Logic In Computer Science ’96, Rutgers; Logic In Computer Science ’97, Warsaw, Chairman; International Conference on Automata Languages and Programming ’98, Aalborg, Co-chairman; CONCUR’99; FOSSACS 2000; WOLLIC’02; CONCUR’03; APPSEM’04; WISP’04; APPSEM’05; CONCUR’05; FOSSACS’05; UFO’07; FICS’08.

Examination and Evaluation duties:

PhD examiner for the universities of Oxford, Cambridge (in Pure Mathematics and Computer Science), University of Copenhagen, Denmark’s Technical University at Lyngby, Edinburgh, Ecole Polytechnique and Ecole Nationale Sup´erieure des Mines, Paris, Manchester, Marseilles, Aalborg, Aarhus, Sussex, Universit´e du Qu´ebec `a Montreal, Rennes and the Free University of Amsterdam. D.Sc. examiner for Sheffield and Aarhus universities. On evaluation committees for research positions, assistant-lectureship, lectureship, readership and professorship positions in Denmark, Sweden, Germany and the UK. EU reviewer. Public Examiner in the Honour School of Mathematics and Computation, Public Examiner in the Honour School of Computation, University of Oxford (1997-2000). MFOCS Examiner in Oxford (Mathematics and CS) 2002-05.

Research projects:

BRICS: Founding director of BRICS (Basic Research in Computer Science), research centre of the Danish Research Foundation in theoretical computer science based primarily at Aarhus University with a budget of over 1 million US dollars a year. BRICS started officially in January 1994. Within BRICS research ranges from the traditional areas of logic, semantics and algorithmics to new initiatives in quantum cryptology jointly with the Physics department. Later the BRICS PhD School was established with an extra 1.5 million dollars a year with Mogens Nielsen as director. See www.brics.dk for information on BRICS activities and researchers. Site leader of EU projects CEDISYS, CLICS I and II, LINEAR, APPSEM. On the steering and programme committees of DART a medium size research collaboration between Aarhus, Aalborg and Copenhagen universities (1992-1994). Holder of a Danish Research Council grant (1989-92). SERC grantholder at Cambridge on “Models and logic for parallel computation” (1985-88). EPSRC grantholder at Cambridge on “Domain theory for concurrency—new categorical foundations” (2005-08). Awarded Leverhulme Trust guest professorship grant, 2009-10. Royal Society Leverhulme Trust Senior Research Fellowship 2010-11.

Teaching and supervision:

I have taught courses at Edinburgh, Aarhus, Pisa, Carnegie-Mellon, Stanford and Cambridge universities and supervised PhD students at Carnegie- Mellon, Cambridge and Aarhus universities. At Cambridge (1984-88) I led study groups for PhD students within my areas, and lectured on Theory of Computation, Formal Languages and Automata Theory, Theory of Programming Languages, Semantics of Programming Languages. The lecture notes for the last two courses, supplemented by material taught at Aarhus to undergraduate and MSc students, led to my book “The Formal Semantics of Programming Languages”, MIT Press, 1993, which is used fairly widely in Europe and the U.S.A. (an Italian translation is available: UTET Libreria, 1999) and half the book has been mechanically verified.1 At Cambridge (2000-) I’ve taught Denotational Semantics, Topics in Concurrency, and Discrete Mathematics, and initiated mini-courses for PhD students.

Supervision at Cambridge 1984-88: At the Computer Laboratory, University of Cambridge I supervised diploma and third year projects in the Semantics of OCCAM (1985), An interpreter and verifier for Petri nets (Roy Marriot, 1986), Verification of concurrent machines represented as Petri nets (Julian Bradfield, 1987).

1Tobias Nipkow: Winskel is (almost) Right: Towards a Mechanized Semantics Textbook. Formal Aspects of Computing 10(2): 171-186 (1998) PhD students at Cambridge 1984-88:

[C1] Jonathon Billington: Coloured Petri Nets.

[C2] Guo-Qiang Zhang: Logic of Domains Later published as a book by Birkhäuser in the Progress in Theor. Comp. Sc. series, 1991.

[C3] Juanito Camilleri: Priority in Process Calculi. Supervision at Aarhus 1988-2000:

[A1] Sten Agerholm and Henrik Skjødt: Automating a model checker for recursive modal asssertions in HOL. Student project, DAIMI IR-92, 1990.

[A2] Sten Agerholm: Program refinement in HOL. MSc thesis, 1992.

[A3] Ann-Grete Tan, Anders Pilegaard and Peter Strarup Jensen: Defining mutually recursive types in HOL. Student project, DAIMI IR-99, 1990.

[A4] Ann-Grete Tan, Anders Pilegaard: Programming with proofs. MSc thesis, 1991.

[A5] Brian Andersen and Carsten Rickers: A low level circuit model in HOL. Student project, 1990.

[A6] Michael Pedersen, Jens Bæk Jørgensen and Rikke Drewsen Andersen. Literal resolution in the propositional calculus using the HOL theorem prover. Student project, 1990.

[A7] Poul Christensen and Hans Jacob Pedersen: Automating mutually recursive type definition in HOL. Student project, DAIMI IR-94, 1990.

[A8] Poul Christensen and Hans Jacob Pedersen: A reformulation of Lamport’s Temporal Logic of Actions. MSc thesis, 1993.

[A9] Ole I. Hougaard. Computability in HOL—a model for computation in formal logic. MSc thesis, 1993.

[A10] Urban Engberg: Analyzing authentication protocols. Student project, DAIMI IR-97, 1990.

[A11] Claus Torp Jensen: The concurrency workbench with priority. Student project, 1992.

[A12] Bettina Blaaberg Sørensen and Christian Clausen: Adequacy results for a lazy functional language with recursive and polymorphic types. Student project, 1992. Published in Theor. Comp. Sc., 1994.

[A13] Henrik Enstrøm: A model of polymorphism in the effective topos. MSc thesis, 1997.

PhD Students at Aarhus 1988-2000:

[A14] Henrik Reif Andersen: Verification of temporal properties of concurrent systems. PhD thesis, June 1993.

[A15] Sten Agerholm: Domain Theory in HOL. PhD thesis, June 1994.

[A16] Claus Torp Jensen: Prioritized and independent actions in distributed computer systems. PhD thesis, August 1994.

[A17] Urban Engberg: Reasoning in the Temporal Logic of Actions, the design and implementation of an interactive computer system. PhD thesis, August 1996.

[A18] Torben Bräuner: An Axiomatic Approach to Adequacy. PhD thesis, November 1996.

[A19] Gian Luca Cattani: Presheaf Models for Concurrency. PhD thesis, May 1999.

[A20] Thomas Troels Hildebrandt: Categories of models for concurrency— independence, fairness and dataflow. PhD thesis, 2000.

PhD Students at Aarhus and Cambridge (2000–):

[A21] Mikkel Nygaard: Domain Theory for Concurrency. PhD thesis, July 2003.

[A22] Mario Jose Caccamo: A Formal Calculus for Categories. PhD thesis, June 2003.

[A23] Federico Crazzolara: Language, Semantics, and Methods for Security Protocols. PhD thesis, May 2003.

[A24] Daniele Varacca: Probability, Nondeterminism and Concurrency two denotational models for probabilistic computation. PhD thesis, November 2003.

[A25] Lucy Saunders-Evans, Event Structures with Persistence. PhD thesis, 2007.

[A26] David Turner, Nominal Domain Theory. PhD thesis, 2009.

[A27] Jonathan Hayman, Petri-net semantics. PhD thesis, 2010. Current PhD students: Christopher Thompson-Walsh; Steffen Loesch

Invitations:

I have been invited to give seminars (often several times), at Computer Science and Mathematics departments at the following universities and institutions: Oxford, Cambridge, Leeds, Birmingham, Swansea, Odense, Technical University Lyngby, Manchester, Warwick, Edinburgh, Hatfield, Surrey, Imperial College, Brunel, INRIA Paris and Sophia Antipolis, Aarhus, Aachen, Eindhoven, Copenhagen, Philips Research Laboratory Eindhoven, Pisa, Berlin, GMD Bonn, Carnegie–Mellon, SRI Palo Alto, Stanford, University of NSW Sydney Australia, University of Macquarie Sidney Australia. I have been invited to lecture at many summerschools, workshops and conferences over the years in topics ranging from concurrency, linear logic, denotational semantics, to hardware verification.

Selected invitations:

• Invited speaker, Category Theory in Computer Science, Cambridge (August 1995)
• Invited lecturer, Isaac Newton Institute Summer School on Semantics of Computation (September 1995)
• Invited participant, Isaac Newton Institute programme in Semantics of Computation (August-December 1995)
• Invited speaker, DIMACS workshop on Partial Order Methods In Verification, Princeton, (July 1996)
• Invited lecturer, CSL’96, Utrecht (September 1996)
• Invited tutorial speaker, CSL’96, Utrecht (September 1996)
• Guest speaker, 10th Anniversary of Laboratory for the Foundations of Computer Science, Edinburgh University (November 1996)
• Invited lecturer, CONCUR’97, Warsaw (July 1997)
• Invited lecturer, MFPS’97, Pittsburgh (March 1997)
• Invited lecturer, Workshop on Domains III, Munich (May 1997)
• Lecturer, School on Computational and Syntactic Methods, De Brug te Mierlo (August 1997)
• Invited speaker, HOOTS II, International Workshop on Higher Order Operational Techniques in Semantics, Stanford University, (December 1997)
• Invited Speaker, AMAST’98, Amazonas, Brazil (January 1999)
• Invited Speaker, British Colloquium in Theoretical Computer Science, Keele (April 1999)
• Invited Speaker, Workshop on Geometric and Topological Methods in Concurrency Theory, Aalborg (June 1999)
• Invited Speaker, 7th Workshop on Logic, Language, Information and Computation (WoLLIC’2000), Natal, Brazil (August 2000)
• Invited Speaker, APPSEM Workshop, Darmstadt, Germany (March 2001)
• Invited Speaker, MFPS ’2000, Aarhus, Denmark (May 2001)
• Invited speaker, FICS’02 workshop. Affiliated with FLoC’02. Copenhagen, Denmark, July 2002.
• Invited speaker, Workshop on Domain Theory in Honour of Dana S. Scott on his 70’th birthday. Affiliated with FLoC’02. Copenhagen, Denmark, July 2002
• Guest professor, Ecole Normale Sup´erieure, Paris, one month 2002
• Categorical Methods in Concurrency, Interaction and Mobility (CMCIM)2003
• Guest lecturer Fields Institute Summer School, Ottawa, June 2003
• Keynote speaker at the LICS’03 workshop on Causality in Computer Science and Physics, Ottawa, June 2003
• Guest professor, Universit´e de Paris Nord, one month 2004
• Invited speaker 3rd International Symposium on Domain Theory (ISDT’03), Xi’an China, May 2004
• Invited speaker WISP’04, Bologna, June 2004
• Invited speaker LICS’05, Chicago, June 2005
• Invited speaker EXPRESS’05, San Francisco, August 2005
• Invited speaker at the 60th Birthday Event in Edinburgh for Gordon Plotkin, September 2006
• Invited speaker Logic Summer School, Canberra Australia, 2006
• Invited speaker USMC’07 Canberra, 2007
• Invited speaker CALCO’07 Bergen, 2007
• Invited speaker at the 60th birthday celebration in Paris, ‘Journées Jean-Yves Girard,’ September 2007
• Invited speaker at CHOCO project theme-day on Event Structures, ENS Lyon, April 2008
• Invited speaker at ‘Concurrency, Graphs and Models’ A Colloquium in Honour of Ugo Montanari on his 65'th birthday, June 2008
• Keynote speaker at the Fifth International Symposium on Domain Theory, Shanghai, September 12-14, 2009
• Invited speaker at the 60th birthday celebration of Mogens Nielsen, Aarhus, September 2009
• Invited speaker at IP 2009 New Orleans, 5-9 October, 2009
• Invited speaker at SAS 2010, Perpignan, 14-16 September, 2010