Claudio Russo's Publications

[1] Sooraj Bhat, Johannes Borgström, Andrew D. Gordon, and Claudio Russo. Deriving probability density functions from probabilistic functional programs. In Proceedings of the 19th international conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'13, pages 508-522, Berlin, Heidelberg, 2013. Springer-Verlag.
[ http ]
[2] Andrew D. Gordon, Mihhail Aizatulin, Johannes Borgstrom, Guillaume Claret, Thore Graepel, Aditya V. Nori, Sriram K. Rajamani, and Claudio Russo. A model-learner pattern for bayesian reasoning. In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '13, pages 403-416, New York, NY, USA, 2013. ACM.
[ http ]
Keywords: bayesian reasoning, machine learning, model-learner pattern, probabilistic programming
[3] Gavin Bierman, Claudio Russo, Geoffrey Mainland, Erik Meijer, and Mads Torgersen. Pause 'n' play: Formalizing asynchronous C#. In James Noble, editor, ECOOP 2012 - Object-Oriented Programming, Lecture Notes in Computer Science. Springer Berlin / Heidelberg, June 2012.
[ http ]
Writing applications that connect to external services and yet remain responsive and resource conscious is a difficult task. With the rise of web programming this has become a common problem. The solution lies in using asynchronous operations that separate issuing a request from waiting for its completion. However, doing so in common object-oriented languages is difficult and error prone. Asynchronous operations rely on callbacks, forcing the programmer to cede control. This inversion of control-flow impedes the use of structured control constructs, the staple of sequential code. In this paper, we describe the language support for asynchronous programming in the upcoming version of C#. The feature enables asynchronous programming using structured control constructs. Our main contribution is a precise mathematical description that is abstract (avoiding descriptions of compiler-generated state machines) and yet sufficiently concrete to allow important implementation properties to be identified and proved correct.
[4] Claudio Russo and Neng Fa Zhou, editors. Fourteenth International Symposium on Practical Aspects of Declarative Languages (PADL 2007), volume 7149 of Lecture Notes In Computer Science (LNCS). Springer-Verlag, January 2012.
[ .pdf ]
[5] Aaron J. Turon and Claudio V. Russo. Scalable Join Patterns. In Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA '11, pages 575-594, New York, NY, USA, 2011. ACM.
[ .pdf ]
Coordination can destroy scalability in parallel programming. A comprehensive library of scalable synchronization primitives is therefore an essential tool for exploiting parallelism. Unfortunately, such primitives do not easily combine to yield solutions to more complex problems. We demonstrate that a concurrency library based on Fournet and Gonthier's join calculus can provide declarative and scalable coordination. By declarative, we mean that the programmer needs only to write down the constraints of a coordination problem, and the library will automatically derive a correct solution. By scalable, we mean that the derived solutions deliver robust performance both as the number of processors increases, and as the complexity of the coordination problem grows. We validate our claims empirically on seven coordination problems, comparing our generic solution to specialized algorithms from the literature.
Keywords: concurrency, message passing, parallelism
[6] Andreas Rossberg, Claudio V. Russo, and Derek Dreyer. F-ing Modules. In 2010 ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI2010), 2010. Coq formalization http://www.mpi-sws.org/~rossberg/f-ing/f-ing.zip.
[ .pdf ]
ML modules are a powerful language mechanism for decomposing programs into reusable components. Unfortunately, they also have a reputation for being complex and requiring fancy type theory that is mostly opaque to non-experts. While this reputation is certainly understandable, given the many non-standard methodologies that have been developed in the process of studying modules, we aim here to demonstrate that it is undeserved. To do so, we give a very simple elaboration semantics for a full-featured, higher-order ML-like module language. Our elaboration defines the meaning of module expressions by a straightforward, compositional translation into vanilla System F-omega (the higher-order polymorphic lambda-calculus), under plain F-omega typing environments. We thereby show that ML modules are merely a particular mode of use of System F-omega.

Our module language supports the usual second-class modules with Standard ML-style generative functors and local module definitions. To demonstrate the versatility of our approach, we further extend the language with the ability to package modules as first-class values-a very simple extension, as it turns out. Our approach also scales to handle OCaml-style applicative functor semantics, but the details are significantly more subtle, so we leave their presentation to a future, expanded version of this paper.

Lastly, we report on our experience using the locally nameless approach in order to mechanize the soundness of our elaboration semantics in Coq.

[7] John Reppy, Claudio Russo, and Yingqi Xiao. Parallel Concurrent ML. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009), September 2009.
[ .pdf ]
Concurrent ML (CML) is a high-level message-passing language that supports the construction of first-class synchronous abstractions called events. This mechanism has proven quite effective over the years and has been incorporated in a number of other languages. While CML provides a concurrent programming model, its implementation has always been limited to uniprocessors. This limitation is exploited in the implementation of the synchronization protocol that underlies the event mechanism, but with the advent of cheap parallel processing on the desktop (and laptop), it is time for Parallel CML. Parallel implementations of CML-like primitives for Java and Haskell exist, but build on high-level synchronization constructs that are unlikely to perform well. This paper presents a novel, parallel implementation of CML that exploits a purpose-built optimistic concurrency protocol designed for both correctness and performance on shared-memory multiprocessors. This work extends and completes an earlier protocol that supported just a strict subset of CML with synchronization on input, but not output events. Our main contributions are a model-checked reference implementation of the protocol and two concrete implementations. This paper focuses on Manticore's functional, continuation-based implementation but briefly discusses an independent, thread-based implementation written in C# and running on Microsoft's stock, parallel runtime. Although very different in detail, both derive from the same design. Experimental evaluation of the Manticore implementation reveals good performance, despite the extra overhead of multiprocessor synchronization.
[8] Claudio V. Russo and Dimitrios Vytiniotis. QML: Explicit First-Class Polymorphism for ML. In 2009: ACM-SIGPLAN Workshop on ML. ACM Press, August 2009. (downloads http://research.microsoft.com/~crusso/qml).
[ .pdf ]
Recent years have seen a revival of interest in extending ML's predicative type inference system with impredicative quantification in the style of System F, for which type inference is undecidable. This paper suggests a modest extension of ML with System F types: the heart of the idea is to extend the language of types with unary universal and existential quantifiers. The introduction and elimination of a quantified type is never inferred but indicated explicitly by the programmer by supplying the quantified type itself. Quantified types co-exist with ordinary ML schemes, which are in turn implicitly introduced and eliminated at let-bindings and use sites, respectively. The resulting language, QML, does not impose any restriction on instantiating quantified variables with quantified types; neither let- nor λ-bound variables ever require a type annotation, even if the variable's inferred scheme or type involves quantified types. This proposal, albeit more verbose in terms of annotations than others, is simple to specify, implement, understand, and formalize.
[9] Claudio Russo. Join Patterns for Visual Basic. In OOPSLA 2008: Proceedings of the 2008 ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. ACM Press, October 2008.
[ .pdf ]
We describe an extension of Visual Basic 9.0 with asynchronous concurrency constructs - join patterns - based on the join calculus. Our design of Concurrent Basic (CB) builds on earlier work on Polyphonic C# and Comega. Since that work, the need for language-integrated concurrency has only grown, both due to the arrival of commodity, multi-core hardware, and the trend for Rich Internet Applications that rely on asynchronous client-server communication to hide latency. Unlike its predecessors, CB adopts an event-like syntax that should be familiar to existing VB programmers. Coupled with Generics, CB allows one to declare re-useable concurrency abstractions that were clumsy to express previously. CB removes its ancestors' inconvenient inheritance restriction, while providing new extensibility points useful in practical applications that must co-exist with or want to exploit alternative threading models available on the platform. CB is implemented as an extension of the production VB 9.0 compiler.
[10] Claudio Russo. The Joins Concurrency Library. In Michael Hanus, editor, Ninth International Symposium on Practical Aspects of Declarative Languages (PADL 2007), volume 4354 of Lecture Notes In Computer Science (LNCS), pages 260-274. Springer-Verlag, January 2007. (c) Springer-Verlag, http://www.springer.de/comp/lncs/index.html.
[ .pdf ]
Comega extended C# 1.x with a simple, declarative and powerful model of concurrency - join patterns - applicable both to multithreaded applications and to the orchestration of asynchronous, event-based distributed applications. With Generics available in C# 2.0, we can now provide join patterns as a library rather than a language feature. The Joins library extends its clients with an embedded, type-safe and mostly declarative language for expressing synchronization patterns. The library has some advantages over Comega: it is language neutral, supporting other languages like Visual Basic; its join patterns are more dynamic, allowing solutions difficult to express with Comega; its code is easy to modify, fostering experimentation. Although presenting fewer optimization opportunities, the implementation is efficient and its interface makes it trivial to translate Comega programs to C#. We describe the interface and implementation of Joins which (ab)uses almost every feature of Generics.
[11] Derek Dreyer and Claudio Russo, editors. ML '07: Proceedings of the 2007 ACM SIGPLAN Workshop on ML, New York, NY, USA, 2007. ACM. 565075.
[12] Burak Emir, Andrew J. Kennedy, Claudio Russo, and Dachuan Yu. Variance and generalized constraints for C# generics. In European Conference on Object-Oriented Programming (ECOOP), July 2006.
[ .pdf ]
Generic types in C# behave invariantly with respect to subtyping. We propose a system of type-safe variance for C# that supports the declaration of covariant and contravariant type parameters on generic types. To support more widespread application of variance we also generalize the existing constraint mechanism with arbitrary subtype assertions on classes and methods. This extension is useful even in the absence of variance, and subsumes equational constraints proposed for Generalized Algebraic Data Types (GADTs). We formalize the subtype relation in both declarative and syntax-directed style, and describe and prove the correctness of algorithms for constraint closure and subtyping. Finally, we formalize and prove a type safety theorem for a featherweight language with variant classes and generalized constraints.
[13] Andrew Kennedy and Claudio Russo. Generalized algebraic data types and object-oriented programming. In OOPSLA 2005: Proceedings of the 2005 ACM Conference on Object-Oriented Programming, Systems, Languages and Applications. ACM Press, October 2005.
[ .pdf ]
Generalized algebraic data types (GADTs) have received much attention recently in the functional programming community. They generalize the type-parameterized datatypes of ML and Haskell by permitting constructors to produce different type-instantiations of the same datatype. GADTs have a number of applications, including strongly-typed evaluators, generic pretty-printing, generic traversals and queries, and typed LR parsing. We show that existing object-oriented programming languages such as Java and C# can express GADT definitions, and a large class of GADT-manipulating programs, through the use of generics, subclassing, and virtual dispatch. However, some programs can be written only through the use of redundant run-time casts. We propose a generalization of the type constraint mechanisms of C# and Java to avoid the need for such casts, present a Visitor pattern for GADTs, and describe a switch construct as an alternative to virtual dispatch on datatypes. We formalize both extensions and prove a type soundness result.
[14] Andrew Kennedy, Nick Benton, Sam Lindley, and Claudio Russo. Shrinking reductions in SML.NET. In 16th International Workshop on Implementation and Application of Functional Languages (IFL '04)., volume 41 of Springer Lecture Notes in Computer Science. Springer Verlag, September 2004.
[ .pdf ]
One performance-critical phase in the SML.NET compiler involves rewriting intermediate terms to monadic normal form and performing non-duplicating beta-reductions. We present an imperative algorithm for this simplification phase, working with a mutable, pointer-based term representation, which significantly outperforms our existing functional algorithm. This is the first implementation and evaluation of a linear-time rewriting algorithm proposed by Appel and Jim.
[15] Nick Benton, Andrew Kennedy, and Claudio V. Russo. Adventures in interoperability: the SML.NET experience. In PPDP '04: Proceedings of the 6th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pages 215-226. ACM Press, August 2004.
[ .pdf ]
SML.NET is a compiler for Standard ML that targets the Common Language Runtime and is integrated into the Visual Studio development environment. It supports easy interoperability with other .NET languages via a number of language extensions, which go considerably beyond those of our earlier compiler, MLj.This paper describes the new language extensions and the features of the Visual Studio plugin, including syntax highlighting, Intellisense, continuous type inference and debugger support. We discuss our experiences using SML.NET to write SML programs that interoperate with other .NET languages, libraries and frameworks. Examples include the Visual Studio plugin itself (written in SML.NET, using .NET's COM interop features to integrate in a C++ application) and writing ASP.NET and Pocket PC applications in SML.
[16] Claudio V. Russo. Types for Modules. Electronic Notes in Theoretical Computer Science, 60, January 2003. This monograph contains an additional chapter not included in the thesis version.
[ .pdf ]
The programming language Standard ML is an amalgam of two, largely orthogonal, languages. The Core language expresses details of algorithms and data structures. The Modules language expresses the modular architecture of a software system. Both languages are statically typed, with their static and dynamic semantics specified by a formal definition.

Over the past decade, Standard ML Modules has been the source of inspiration for much research into the type-theoretic foundations of modules languages. Despite these efforts, a proper type-theoretic understanding of its static semantics has remained elusive. In this thesis, we use Type Theory as a guideline to reformulate the unconventional static semantics of Modules, providing a basis for useful extensions to the Modules language.

Our starting point is a stylised presentation of the existing static semantics of Modules, parameterised by an arbitrary Core language. We claim that the type-theoretic concepts underlying Modules are type parameterisation, type quantification and subtyping. We substantiate this claim by giving a provably equivalent semantics with an alternative, more type-theoretic presentation. In particular, we show that the notion of type generativity corresponds to existential quantification over types. In contrast to previous accounts, our analysis does not involve first-order dependent types.

Our first extension generalises Modules to higher-order, allowing modules to take parameterised modules as arguments, and return them as results. We go beyond previous proposals for higher-order Modules by supporting a notion of type generativity. We give a sound and complete algorithm for type-checking higher-order Modules. Our second extension permits modules to be treated as first-class citizens of an ML-like Core language, greatly extending the range of computations on modules. Each extension arises from a natural generalisation of our type-theoretic semantics.

This thesis also addresses two pragmatic concerns. First, we propose a simple approach to the separate compilation of Modules, which is adequate in practice but has theoretical limitations. We suggest a modified syntax and semantics that alleviates these limitations. Second, we study the type inference problem posed by uniting our extensions to higher-order and first-class modules with an implicitly-typed, ML-like Core language. We present a hybrid type inference algorithm that integrates the classical algorithm for ML with the type-checking algorithm for Modules.

[17] Claudio V. Russo. Recursive Structures for Standard ML. In Proceedings of the 2001 ACM SIGPLAN International Conference on Functional Programming, pages 50-61. ACM Press, September 2001.
[ .pdf ]
Standard ML is a statically typed programming language that is suited for the construction of both small and large programs. Programming in the small is captured by Standard ML's Core language. Programming in the large is captured by Standard ML's Modules language that provides constructs for organizing related Core language definitions into self-contained modules with descriptive interfaces. While the Core is used to express details of algorithms and data structures, Modules is used to express the overall architecture of a software system. In Standard ML, modular programs must have a strictly hierarchical structure: the dependency between modules can never be cyclic. In particular, definitions of mutually recursive Core types and values, that arise frequently in practice, can never span module boundaries. This limitation compromises modular programming, forcing the programmer to merge conceptually (i.e. architecturally) distinct modules. We propose a practical and simple extension of the Modules language that caters for cyclic dependencies between both types and terms defined in separate modules. Our design leverages existing features of the language, supports separate compilation of mutually recursive modules and is easy to implement.
[18] Gavin M. Bierman, Andrew M. Pitts, and Claudio V. Russo. Operational properties of Lily, a polymorphic linear lambda calculus with recursion. In Fourth International Workshop on Higher Order Operational Techniques in Semantics, Montréal, volume 41 of Electronic Notes in Theoretical Computer Science. Elsevier, September 2000.
[ .pdf ]
Plotkin has advocated the combination of linear lambda calculus, polymorphism and fixed point recursion as an expressive semantic metalanguage. We study its expressive power from an operational point of view. We show that the naturally call-by-value operators of linear lambda calculus can be given a call-by-name semantics without affecting termination at exponential types and hence without affecting ground contextual equivalence. This result is used to prove properties of a logical relation that provides a new extensional characterisation of ground contextual equivalence and relational parametricity properties of polymorphic types.
[19] Claudio V. Russo. First-class Structures for Standard ML. In Programming Languages and Systems, ESOP 2000, volume 1782, pages 336-350. Springer Verlag, March 2000.
[ .pdf ]
Standard ML is a statically typed programming language that is suited for the construction of both small and large programs. Programming in the small is captured by Standard ML's Core language. Programming in the large is captured by Standard ML's Modules language that provides constructs for organising related Core language definitions into self-contained modules with descriptive interfaces. While the Core is used to express details of algorithms and data structures, Modules is used to express the overall architecture of a software system. The Modules and Core languages are stratified in the sense that modules may not be manipulated as ordinary values of the Core. This is a limitation, since it means that the architecture of a program cannot be reconfigured according to run-time demands. We propose a novel extension of the language that allows modules to be manipulated as first-class values of the Core language. The extension greatly extends the expressive power of the language and has been shown to be compatible with both Core type inference and a separate extension to higher-order modules.
[20] Claudio V. Russo. First-class Structures for Standard ML. Nordic Journal Of Computing, 7:348-374, January 2000. Copy available on request.
[ http ]
Standard ML is a statically typed programming language that is suited for the construction of both small and large programs. ``Programming in the small'' is captured by Standard ML's Core language. ``Programming in the large'' is captured by Standard ML's Modules language that provides constructs for organising related Core language definitions into self-contained modules with descriptive interfaces. While the Core is used to express details of algorithms and data structures, Modules is used to express the overall architecture of a software system. The Modules and Core languages are stratified in the sense that modules may not be manipulated as ordinary values of the Core. This is a limitation, since it means that the architecture of a program cannot be reconfigured according to run-time demands. We propose a novel and practical extension of the language that allows modules to be manipulated as first-class values of the Core language.
[21] Claudio V. Russo. Non-dependent types for Standard ML Modules. In PPDP '99: Proceedings of the International Conference PPDP'99 on Principles and Practice of Declarative Programming, pages 80-97. Springer-Verlag, September 1999.
[ .pdf ]
Two of the distinguishing features of Standard ML Modules are its term dependent type syntax and the use of type generativity in its static semantics. From a type-theoretic perspective, the former suggests that the language involves first-order dependent types, while the latter has been regarded as an extra-logical device that bears no direct relation to type-theoretic constructs. We reformulate the existing semantics of Modules to reveal a purely second-order type theory. In particular, we show that generativity corresponds precisely to existential quantification over types and that the remainder of the Modules type structure is based exclusively on the second-order notions of type parameterisation, universal type quantification and subtyping. Our account is more direct than others and has been shown to scale naturally to both higher-order and first-class modules.
[22] Claudio V. Russo. Types for Modules. PhD thesis, Edinburgh University, Edinburgh, Scotland, March 1998. LFCS Thesis ECS-LFCS-98-389. [16] is a version of this document with an additional chapter on Moscow ML, proper bookmarks, and hyper links.
[ .pdf ]
The programming language Standard ML is an amalgam of two, largely orthogonal, languages. The Core language expresses details of algorithms and data structures. The Modules language expresses the modular architecture of a software system. Both languages are statically typed, with their static and dynamic semantics specified by a formal definition.

Over the past decade, Standard ML Modules has been the source of inspiration for much research into the type-theoretic foundations of modules languages. Despite these efforts, a proper type-theoretic understanding of its static semantics has remained elusive. In this thesis, we use Type Theory as a guideline to reformulate the unconventional static semantics of Modules, providing a basis for useful extensions to the Modules language.

Our starting point is a stylised presentation of the existing static semantics of Modules, parameterised by an arbitrary Core language. We claim that the type-theoretic concepts underlying Modules are type parameterisation, type quantification and subtyping. We substantiate this claim by giving a provably equivalent semantics with an alternative, more type-theoretic presentation. In particular, we show that the notion of type generativity corresponds to existential quantification over types. In contrast to previous accounts, our analysis does not involve first-order dependent types.

Our first extension generalises Modules to higher-order, allowing modules to take parameterised modules as arguments, and return them as results. We go beyond previous proposals for higher-order Modules by supporting a notion of type generativity. We give a sound and complete algorithm for type-checking higher-order Modules. Our second extension permits modules to be treated as first-class citizens of an ML-like Core language, greatly extending the range of computations on modules. Each extension arises from a natural generalisation of our type-theoretic semantics.

This thesis also addresses two pragmatic concerns. First, we propose a simple approach to the separate compilation of Modules, which is adequate in practice but has theoretical limitations. We suggest a modified syntax and semantics that alleviates these limitations. Second, we study the type inference problem posed by uniting our extensions to higher-order and first-class modules with an implicitly-typed, ML-like Core language. We present a hybrid type inference algorithm that integrates the classical algorithm for ML with the type-checking algorithm for Modules.


This file has been generated by bibtex2html 1.74