Aaron TuronPhD studentCollege of Computer and Information Science Northeastern University turon at ccs dot neu dot edu |
|
Research advisor: Mitch Wand
Research interests: concurrency, process algebra, verification, logic, type theory, programming language semantics and design.
PL Seminar, Jr.
I am the current organizer for PL Seminar, Jr., a weekly programming languages seminar for PhD students. Presentations are usually surveys of established work, rather than talks about current research, as the latter is the focus of Mitch Wand's PL Seminar. The two seminars address distinct needs, and students are encouraged to attend both.Publications
Aaron Turon and Mitchell Wand. A separation logic for the pi-calculus. Submitted.
[ pdf]Panagiotis Manolios and Aaron Turon. All-Termination(SCP). To appear.
[ pdf | slides ]Panagiotis Manolios and Aaron Turon. All-Termination(T). In Tools and Algorithms for the Construction and Analysis of Systems, March 2009.
[ pdf | slides ]Scott Owens, John Reppy, and Aaron Turon. Regular expression derivatives reexamined. To appear, Journal of Functional Programming.
[ pdf ]Aaron Turon. Metaprogramming with Traits. (honors thesis)
[ pdf ]John Reppy and Aaron Turon. Metaprogramming with Traits. In European Conference on Object-Oriented Programming, July 2007.
[ pdf ]John Reppy and Aaron Turon. A foundation for trait-based metaprogramming. In online proceedings for FOOL/WOOD '06, January 2006.
[ pdf | slides | tech report ]
Drafts
Aaron Turon. Burke-Fisher error repair in a recursive-descent parser.
Other documents
SML/NJ Language Processing Tools: User Guide.
[ pdf ]ML-Flex implementation notes (somewhat outdated).
[ pdf ]
Projects
Separation logic for mobile processes
With Mitch Wand, I am exploring applications of separation logic to message-passing concurrency. We have developed a logic for the pi-calculus that combines temporal and separation logic, and treats channels as resources that can be gained and lost by processes. The resource model provides a lightweight way to constrain interference.The join calculus
The join calculus is a process calculus for distributed programming, inspired by both the pi-calculus and Berry and Boudol's Chemical Abstract Machine. With Mitch Wand, I am working toward a study of type systems and other static analyses for the join calculus.Termination analysis
I'm investigating a variety of extensions to Manolios and Vroon's termination analysis, which is based on "calling context graphs". These extensions include higher-order variants, abstraction/refinement techniques, counterexample generation, and more sophisticated induction scheme generation. This work is supervised by Pete Manolios.Traits
Traits are a simple mechanism for structuring classes within a single-inheritance language; essentially, a trait is just a collection of fields and methods that can be incorporated into many classes, even when only single-inheritance is allowed. Thus, traits are very similar to mixins. The main distinction is composition: mixins are composed by successive inheritance, which forces a linear order on the mixins to be composed. In contrast, traits are composed in a symmetric fashion, and conflicts are not allowed. To make this practical, languages generally allow aliasing and exclusion of trait members during composition.In many domains, it is common for classes to have highly regular internal structure. A simple example is the use of "setters" and "getters" for private instance variables. A more compelling example is the use of "business objects" to represent pertinent business entities and to persist information about those entities to a database. Such objects often contain boilerplate code for mapping database fields to class members, and this code must be repeated per-field, per-class. My research on traits has focused on their use as a means of specifying repetitive structure within a single class. Traits are well-suited for this task, once they are outfitted with an appropriate mechanism for abstraction.
My honors thesis (and companion paper), Metaprogramming with Traits, explores these ideas in depth, and presents a typed calculus of abstractable traits. I show that, with a modest set of operations, traits can be used to cleanly capture a wide variety of previously unabstractable code.
SML/NJ
With John Reppy, I have rewritten the lexical analyzer generator ML-Lex. The new implementation is based on Brzozowski's regular expression derivatives (see this page for a short introduction). Notable new features include Unicode support and a more complete set of operations on regular expressions (e.g., complement and intersection).Using Terence Parr's linear-approximate lookahead, LL(k) parsing is practical even when k>1. We have designed and implemented an LL(k) parser generator for SML/NJ. The new tool is similar in spirit to Parr's ANTLR. There are numerous advantages to LL(k) parsers: because they are predictive, information can flow down as well as up the grammar as the parse takes place. The LL(k) restriction is easier to understand than the LALR(1) restriction, a boon for grammar-writing. We can go beyond LL(k) by introducing selective backtracking and semantic predicates. Additional features of note include grammar inheritance for language extension, support for EBNF-style specifications and robust, automatic error repair.
Moby
John Reppy and Kathleen Fisher developed Moby as an experiment in adding classes, objects, and concurrency to an SML-like language. I have been involved in the implementation of separate compilation for Moby, and hope in the future to add traits to the language.
Music
Probably my favorite hobby, when I have the time for it--rarely, these days--is writing music.A few songs:
Justcraft