Claudio Russo (Postdoctoral Research Fellow)

... a long time ago on bad hair day.

I am a research fellow in the LFCS, a group in the Division of Informatics, University of Edinburgh, Scotland.

Current Research Project

At the moment, I am applying the results of my thesis to design and implement an  extension of  Standard ML  with higher-order and first-class modules. The end product of this work will be an (un-official) revised Definition of Standard ML and a byte-code compiler built on top of Moscow ML. I have completed a draft of the formal definition of the static semantics and am in the process of implementing the compiler.

Research interests

Module systems, programming language design and implementation, Type Theory, operational semantics, interactive and automated theorem proving, software engineering.


Claudio V. Russo. First-Class Structures for Standard ML. An earlier version of a paper submitted to 2000 International Conference on Principles of Programming Languages. 1999. 21 pages.
Claudio V. Russo. Non-Dependent Types for Standard ML Modules . Preliminary version accepted at 1999 Int'l Conf. on Principles and Practice of Declarative Programming. 18 pages.
Claudio V. Russo. The Definition of Non-Standard ML. Draft (available on request).
Claudio V. Russo. Types For Modules. University of Edinburgh, LFCS thesis ECS-LFCS-98-389. 1998. 360 pages. (Also available from the LFCS repository.)
Claudio V. Russo. An implementation of higher-order and first-class modules.
This is the source code for a prototype interpreter that accompanies my thesis [4].
(Available as a gzipped tar file, 28 Kbytes. For further details, see the accompanying readme file, reproduced here).
Claudio V. Russo. Standard ML Type Generativity as Existential Quantification. University of Edinburgh, LFCS report ECS-LFCS-96-344. 1996. 19 pages. (Also available from the LFCS repository).
Claudio V. Russo. Automating Mutually Recursive Type Definitions in HOL. University of Edinburgh, 4th Year Undergraduate Project Report. 1992. 59 pages..


Claudio V. Russo. Non-Dependent Types for Modules. Presented at 1999 Workshop on Dependent Types in Programming, Gothenburg, Sweden. 21 pages.
Claudio V. Russo. Types for Modules. Presented at a Computer Science Colloquium, Department of Computer Science, University of Edinburgh. 25 pages.
Claudio V. Russo. Types for Higher-Order Modules. Presented at the LFCS ML Club, Department of Computer Science, University of Edinburgh. 29 pages.

Personal Details

Feel free to have a look at my  curriculum vitae: academic version, commercial version .

Claudio Russo
Laboratory for Foundations of Computer Science
Division of Informatics
University of Edinburgh
JCMB Room  1406
King's Buildings
Mayfield Road
Edinburgh EH9 3JZ
From July 24, 1999 you should send post to, or call me at, my new home address in Cambridge, England:
180 Sturton Street
Cambridge CB1 2QF
Phone: +44 (131) 650 5163 (office) +44 (1223) 474 845 (home in Cambridge)
Fax: +44 (131) 667 7209

  My FTP area