Tuesday, May 17, 2011
N
Monday, May 02, 2011
The N PL semantics tool, and other stuff
Most excitingly (for me) I've been working on a tool for PL researchers called N. It is kind of a proof assistant, but also checks formal type systems and outputs them in pretty LaTeX, so takes out a lot of the drudgery of writing formal type systems. It is very much work in progress, but most of the checking and LaTeX output stuff is done (for a fairly small formal lanaguage) and I am working on the proof assistant part. This is novel (and exiciting for me to work on) because it is purely syntactic and high level, as opposed to Coq, Isabelle etc. which are semantic and low level, http://www.blogger.com/img/blank.gifi.e., they work at the level of logic/maths, whereas N works at the level of PL-style type systems. This means that when N says a proof is done it does not guarantee that the proof is correct. However, writing proofs in N should be orders of magnitude simpler and quicker than using a proper proof assistant. Think of it as a tool for doing hand-written proofs - it does some checking and automates some parts, but does not fully check.
N is written in Python and will be open source very soon (next few days), it will be at https://github.com/nick29581/N. Feedback is appreciated!
Thursday, February 24, 2011
IWACO '11 website
Visit for the latest info on this year's IWACO, which should be a good one as we celebrate 20 years of research in the field.
IWACO 2011: Call for Papers
Call For Papers
International Workshop on Aliasing, Confinement and Ownership
in object-oriented programming (IWACO)
Celebrating 20 years of aliasing research
at ECOOP 2011
July 25th, 2011, Lancaster, UK
http://ecs.victoria.ac.nz/Events/IWACO2011/
Call For Papers
===============
2011 is the 20th anniversary of "The Geneva Convention on The Treatment
of Object Aliasing", which started research in aliasing and led to the
development of object-ownership techniques. To celebrate, IWACO 2011
will be a special edition; we are in negotiation to publish a book
(edited by members of the organising committee) containing the best
papers from IWACO '11 and invited papers of a survey or retrospective
nature. In addition to original research papers, we encourage authors to
submit position papers and papers considering future research
directions.
The power of objects lies in the flexibility of their interconnection
structure. But this flexibility comes at a cost. Because an object can
be modified via any alias, object-oriented programs are hard to
understand, maintain, and analyse. Aliasing makes objects depend on
their environment in unpredictable ways, breaking the encapsulation
necessary for reliable software components, making it difficult to
reason about and optimise programs, obscuring the flow of information
between objects, and introducing security problems.
Aliasing is a fundamental difficulty, but we accept its presence.
Instead we seek techniques for describing, reasoning about, restricting,
analysing, and preventing the connections between objects and/or the
flow of information between them. Promising approaches to these problems
are based on ownership, confinement, information flow, sharing control,
escape analysis, argument independence, read-only references, effects
systems, and access control mechanisms.
The workshop will generally address the question how to manage
interconnected object structures in the presence of aliasing. In
particular, we will consider the following issues (among others):
* models, type and other formal systems, programming language
mechanisms, analysis and design techniques, patterns and notations for
expressing object ownership, aliasing, confinement, uniqueness, and/or
information flow.
* optimisation techniques, analysis algorithms, libraries, applications,
and novel approaches exploiting object ownership, aliasing, confinement,
uniqueness, and/or information flow.
* empirical studies of programs or experience reports from programming
systems designed with these issues in mind
* novel applications of aliasing management techniques such as ownership
types, ownership domains, confined types, region types, and uniqueness.
We encourage not only submissions presenting original research results,
but also papers that attempt to establish links between different
approaches and/or papers that include survey material. Original research
results should be clearly described, and their usefulness to
practitioners outlined. Paper selection will be based on the quality of
the submitted material.
The workshop will be held as part of the ECOOP'11 conference taking
place in Lancaster, England.
Programme Committee
-------------------
Nicholas Cameron (chair, Victoria University of Wellington)
Dave Clarke (KU Leuven)
Werner Dietl (University of Washington)
Ioannis Kassios (ETH Zurich)
Doug Lea (State University of New York at Oswego)
James Noble (Victoria University of Wellington)
Matthew Parkinson (Microsoft Research, Cambridge)
Alex Potanin (Victoria University of Wellington)
Tobias Wrigstad (Uppsala University)
Important Dates
---------------
15 April, 2011: paper submission deadline
20 May, 2011: author notification
25 May, 2011: full program disseminated
24 June, 2011: papers available
25 July, 2011: workshop takes place
Organisers
----------
Dave Clarke (KU Leuven)
James Noble (Victoria University of Wellington)
Tobias Wrigstad (Uppsala University)
Peter Muller (ETH Zurich)
Matthew Parkinson (Microsoft Research, Cambridge)
Participation
-------------
The number of participants is limited to 25. Apart from those with
accepted papers, others may attend by sending an email to Nicholas
Cameron (ncameron@ecs.vuw.ac.nz) indicating what contribution you could
make to the workshop. A small number of places will be reserved for PhD
students and other researchers wishing to begin research in this area.
Selection Process
-----------------
Both full papers (up to 10 pgs.) and short papers (1-2 pgs.) are
welcome. All submissions will be reviewed by the programme committee.
The accepted papers, after rework by the authors, will be published in
the Workshop Proceedings, which will be distributed at the workshop. All
accepted submissions shall remain available from the workshop web page.
Papers should be submitted via Easychair at
https://www.easychair.org/conferences/?conf=iwaco11
by 15 April, 2011. Submissions should be in English.
Queries
-------
Queries may be directed to Nicholas Cameron (ncameron@ecs.vuw.ac.nz).
Christchurch Earthquake
Tuesday, December 21, 2010
Things I'll miss about Wellington
People's Coffee - excellent coffee, even by NZ standards
The Engine Room - a great place for climbing training
The Rak - Not the best climbing spot on earth, but the one I've spent the most time, and I've grown to really like some of the problems
Prana - vegetarian cafe in Newtown - awesome
Cafes in general - including Sweet Mother's, Baobob, Cafe Deluxe, Midnight Espresso, Esspressoholic, Fidel's, Lido, O Sushi
The art gallery (I went to Roundabout the other day and it was excellent, as have been may other exhibits)
The Embassy - such a cool cinema
Our house - it might be small, but it is lovely, and my wife and I's first home together, adn it has an amazingly sunny deck
Two surprisingly good Hip-hop nights at the San Fran Bathhouse (Jean Grae, Talib Kweli, Pharaoh Monch, Mr Len)
The Powerhouse - surely the best place on earth to lift weights (no frills, all hardcore)
Bars - Havana, Monteray, Good Luck, Southern Cross (some weird and cool live music nights), Alice, Motel
All my friends and colleagues - of course!
Links in JOT posts
JOT blog repost: OOPSLA day 3 (finally)
Homogeneous Family Sharing - Xin Qi
Xin talked about extending sharing from classes to class families in the J& family of languages. Sharing is a kind of bidirectional inheritance, and is a language-level alternative to the adapter design pattern. The work includes formalism, soundness proof, and implementation using Polyglot. Dispatch is controlled by the view of an object, the view can be changed by a cast-like operation.
I didn't quite get shadow classes, but I think they are like further bound classes in Tribe.
Finally, their families are open, as in open classes, so the programmer can add classes to families post hoc.
Mostly Modular Compilation of Crosscutting Concerns by Contextual Predicate Dispatch - Shigeru Chiba
Shigeru presented a halfway language between OOP and AOP called GluonJ. The idea is that it should be a more modular version of aspects (I think). However, it was found to be not as modular to check and compile as standard OOP. The language supported cross-cutting concerns with predicate dispatch and an enhanced overriding mechanism.
Ownership and Immutability in Generic Java - Yoav Zibin
Yoav talked about work that combined ownership and immutability in a single system using Java's generics. It is nice work, but I'm afraid I was too busy being nervous about being next up to write any notes.
Tribal Ownership - Nick Cameron (me!)
I talked about work with James Noble and Tobias Wrigstad on using a language with virtual classes (Tribe) to support object ownership (i.e., ownership types without the extra type annotations) for free (that is, no additional programmer syntax overhead). I really like this work, it all seems to come together so neatly, which I find pretty satisfying. I really do think virtual classes are extraordinarily powerful and yet easy enough for programmers to understand. Hopefully, they'll make it into a mainstream language before too long...
A Time-Aware type System for Data-Race Protection and Guaranteed Initialization - Nicholas Matsakis
Nicholas introduced a language (Harmony) where intervals of 'time' are represented in the type system to make the language time-aware. This can be used to prevent race conditions in concurrent programs and for other uses (including some non-concurrent ones), such as allowing new objects time to establish their invariants. Intervals are scoped and an ordering may be specified by the programmer; the runtime or compiler may reorder execution subject to this ordering. Checking is modular and is flow insensitive.
Wednesday, November 17, 2010
OOPSLA day 2 (belated) (JOT repost)
NOTE: I've come back to my notes about the last two days of OOPSLA; it's two weeks since the conference ended, and my memory is already kind of hazy, so the quality of these last two posts might be less than ideal... and another week and a half has passed before I finished even the first of the last two posts, still, better late than never, eh?
Creativity: Sensitivity and Surprise - Benjamin Pearce
Benjamin gave the oddest invited talk I've ever seen. He talked about various aspects of creativity over a large set of photographs, including some of his own. The photos were beautiful and made a great show. Not entirely sure what it has to do with programming, languages, systems, or applications, except at the most abstract level. Still an interesting talk, and it seemed to go down very well with the audience too.
Specifying and Implementing Refactorings - Max Schaffer
Automatic refactoring is popular, and correct in the common cases, but specifications are imperfect. The current `best practice' (e.g., in Eclipse) is to use a bunch of preconditions, but this is not ideal for automatic tools because it is difficult to identify all necessary preconditions; so refactoring sometimes fails, even if all the preconditions are satisfied.
The authors previously suggested specifications based on dependencies and breaking refactorings down into smaller pieces. In this work, they show that this idea actually works for proper refactorings. The dependencies are static and semantic, e.g., constraints on synchronisation and name binding. The authors specified and implemented 17 refactorings.
What can the GC compute efficiently? - Christoph Reichenbach
Christoph presented a system which checks assertions when the garbage collector is run. These assertions are about objects and relations between objects in the heap. This is a pretty efficient way to check heap assertions because the heap must be traversed anyway to do GC. There is a single-touch property - i.e., each assertion can only touch each object once - so checking the assertions is very fast. Their assertion language can describe reachability, dominance, and disjointness, and assertions can be combined with the usual logical operators. Interestingly, garbage collection must be re-ordered to check for reachability and dominance.
Type Classes as Objects and Implicits - Bruno Oliveira
This work `encodes' Haskell type classes in Scala using generics and implicits (the latter being a Scala feature that enables the programmer to omit some parameters). My understanding of the work was that type classes can be done using only generics, but implicits are required to make the `encoding' usable by a programmer. There is a whole lot of other complex-Scala-type-system stuff - I have notes about type members and dependent method types, but I can't remember why...
The interesting thing is that you end up with a really, really powerful language feature: as well as type classes, you can encode session types, which I find incredible (although according to the paper, you can do this with Haskell type classes).
Supporting Dynamic, Third-Party Code Customizations in JavaScript using Aspects
The authors are motivated by the popularity of JavaScript, both on the web and to customise browsers. Such scripts typically rely heavily on code injection, that is inserting new code into existing scripts. This is a pretty ugly process all round - it's as non-modular as you can imagine and implemented in totally unchecked and unsafe ways (mostly monkey patching). The authors propose doing it with aspect-style weaving instead, but claim it's not really aspects, apparently. Weaving is done by the JIT. Their empirical results show that their approach is sufficiently expressive for most use.
Saturday, November 06, 2010
Papers
I still have a couple of blog posts to write up about the last two days at OOPSLA, these should be coming shortly (I was on holiday for a week after OOPSLA and have been kind of busy since I got back).