[1] |
Andrew D. Gordon, Claudio Russo, Marcin Szymczak, Johannes Borgstroem, Nicolas
Rolland, Thore Graepel, and Daniel Tarlow.
Probabilistic programs as spreadsheet queries.
In Jan Vitek, editor, Programming Languages and Systems, volume
9032 of Lecture Notes in Computer Science, pages 1-25. Springer Berlin
Heidelberg, 2015.[ http ] We describe the design, semantics, and implementation of a probabilistic programming language where programs are spreadsheet queries. Given an input database consisting of tables held in a spreadsheet, a query constructs a probabilistic model conditioned by the spreadsheet data, and returns an output database determined by inference. This work extends probabilistic programming systems in three novel aspects: (1) embedding in spreadsheets, (2) dependently typed functions, and (3) typed distinction between random and query variables. It empowers users with knowledge of statistical modelling to do inference simply by editing textual annotations within their spreadsheets, with no other coding. |

[2] |
Andrew D. Gordon, Thore Graepel, Nicolas Rolland, Claudio Russo, Johannes
Borgstrom, and John Guiver.
Tabular: A schema-driven probabilistic programming language.
In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on
Principles of Programming Languages, POPL '14, pages 321-334, New York, NY,
USA, 2014. ACM.[ http ] We propose a new kind of probabilistic programming language for machine learning. We write programs simply by annotating existing relational schemas with probabilistic model expressions. We describe a detailed design of our language, Tabular, complete with formal semantics and type system. A rich series of examples illustrates the expressiveness of Tabular. We report an implementation, and show evidence of the succinctness of our notation relative to current best practice. Finally, we describe and verify a transformation of Tabular schemas so as to predict missing values in a concrete database. The ability to query for missing values provides a uniform interface to a wide variety of tasks, including classification, clustering, recommendation, and ranking. Keywords: bayesian reasoning, machine learning, model-learner pattern, probabilistic programming, relational data |

[3] |
Andreas Rossberg, Claudio Russo, and Derek Dreyer.
F-ing modules.
Journal of Functional Programming, 24:529-607, 2014.[ http ] 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 present a novel formalization of ML modules, which defines their semantics directly by a compositional “elaboration” translation into plain System F_ω (the higher-order polymorphic λ-calculus). To demonstrate the scalability of our “F-ing” semantics, we use it to define a representative, higher-order ML-style module language, encompassing all the major features of existing ML module dialects (except for recursive modules). We thereby show that ML modules are merely a particular mode of use of System F_ω. |

[4] |
Sooraj Bhat, Johannes Borgstrm, 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 ] A Bayesian model is based on a pair of probability distributions, known as the prior and sampling distributions. A wide range of fundamental machine learning tasks, including regression, classification, clustering, and many others, can all be seen as Bayesian models. We propose a new probabilistic programming abstraction, a typed Bayesian model, which is based on a pair of probabilistic expressions for the prior and sampling distributions. A sampler for a model is an algorithm to compute synthetic data from its sampling distribution, while a learner for a model is an algorithm for probabilistic inference on the model. Models, samplers, and learners form a generic programming pattern for model-based inference. They support the uniform expression of common tasks including model testing, and generic compositions such as mixture models, evidence-based model averaging, and mixtures of experts. A formal semantics supports reasoning about model equivalence and implementation correctness. By developing a series of examples and three learner implementations based on exact inference, factor graphs, and Markov chain Monte Carlo, we demonstrate the broad applicability of this new programming pattern. |

[5] |
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 ] A Bayesian model is based on a pair of probability distributions, known as the prior and sampling distributions. A wide range of fundamental machine learning tasks, including regression, classification, clustering, and many others, can all be seen as Bayesian models. We propose a new probabilistic programming abstraction, a typed Bayesian model, which is based on a pair of probabilistic expressions for the prior and sampling distributions. A sampler for a model is an algorithm to compute synthetic data from its sampling distribution, while a learner for a model is an algorithm for probabilistic inference on the model. Models, samplers, and learners form a generic programming pattern for model-based inference. They support the uniform expression of common tasks including model testing, and generic compositions such as mixture models, evidence-based model averaging, and mixtures of experts. A formal semantics supports reasoning about model equivalence and implementation correctness. By developing a series of examples and three learner implementations based on exact inference, factor graphs, and Markov chain Monte Carlo, we demonstrate the broad applicability of this new programming pattern. Keywords: bayesian reasoning, machine learning, model-learner pattern, probabilistic programming |

[6] |
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. |

[7] |
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. |

[8] |
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 |

[9] |
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 |

[10] |
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. |

[11] |
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 |

[12] |
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. |

[13] |
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. |

[14] |
Derek Dreyer and Claudio Russo, editors.
ML '07: Proceedings of the 2007 ACM SIGPLAN Workshop on ML,
New York, NY, USA, 2007. ACM.
565075. |

[15] |
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. |

[16] |
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 |

[17] |
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. |

[18] |
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. |

[19] |
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. |

[20] |
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. |

[21] |
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, Montral, 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. |

[22] |
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. |

[23] |
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. |

[24] |
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. |

[25] |
Claudio V. Russo.
Types for Modules.
PhD thesis, Edinburgh University, Edinburgh, Scotland, March 1998.
LFCS Thesis ECS-LFCS-98-389. [19] 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. |

*This file has been generated by
bibtex2html 1.74*