Previous week Up Next week


Here is the latest Caml Weekly News, for the week of March 11 to 18, 2008.

  1. Oregon Programming Languages Summer School
  2. BDDs in ocaml
  3. is there a Roman Numeral library
  4. Xmlm 1.0.0

Oregon Programming Languages Summer School


Yannis Smaragdakis announced:
The Oregon PL Summer School will run July 22-30, 2008 with the topic "Logic
and Theorem Proving in Programming Languages". This is a very exciting topic,
and we've put together a great collection of speakers. The school has a long
tradition and is sponsored by the NSF, ACM SIGPLAN, and Microsoft Research.
The full "Call for Participation" may be found below.

Matthew Fluet & Yannis Smaragdakis (OPLSS'08 Organizers)


                     Call for Participation:
Summer School on Logic and Theorem Proving in Programming Languages
                         July 22-30, 2008
              University of Oregon (Eugene, Oregon)

This Summer School will cover current research focused on integrating
expressive logical systems and powerful theorem-proving assistants
into the design, definition, and implementation of programming
languages. Speakers will present material covering foundational
theory, advanced techniques, and applications.

Material will be presented at a tutorial level that will help graduate
students and researchers from academia or industry understand the
critical issues and open problems confronting the field. The course is
open to anyone interested. Prerequisites are an elementary knowledge
of logic and mathematics that is usually covered in undergraduate
classes on discrete mathematics. Some knowledge of programming
languages at the level provided by an undergraduate survey course will
also be expected. Our primary target group is PhD students. We also
expect attendance by faculty members who would like to conduct
research on this topic or introduce new courses at their universities.

The program consists of more than twenty-five, 80 minute lectures
presented by internationally recognized leaders in programming
languages and formal reasoning research. Topics include:

SMT Solvers - Theory, Implementation and Applications
   Leonardo de Moura, Microsoft Research
Mechanization of Metatheory using LF and Twelf
   Robert Harper, Carnegie Mellon University
Compiler Construction in Formal Logical Frameworks
   Jason Hickey, California Institute of Technology
Specification and Verification of Programs with Pointers
   Rustan Leino, Microsoft Research
Leveraging Domain-Specific Languages for Reasoning
   Sorin Lerner, University of California - San Diego
Reasoning About Programs with ACL2
   Pete Manolios, Northeastern University
Putting the Curry-Howard Isomorphism to Work
   Tim Sheard, Portland State University
Nominal Techniques
   Christian Urban, TU Munich
Coq for Programming Language Metatheory
   Stephanie Weirich, University of Pennsylvania

The summer school will be held at the University of Oregon, located in
the southern Willamette Valley city of Eugene, close to some of the
world's most spectacular beaches, mountains, lakes and forests. On
Sunday, July 27, students will have the option of participating in a
group activity in Oregon's countryside.

The cost for registration is $175.00 (USD) for graduate students, and
$275.00 (USD) for other participants. Registration must be paid upon
acceptance to the summer school, and is non-refundable. There are a
limited number of grants available to fund part of the cost of student
participation. If you are a graduate student and want to apply for
grant money to cover your expenses, please also include a statement of
your needs with your registration.
Additional information about the program, registration, venue, and
housing options is available on the web site. Or, you may request more
information by email.
To register for the Summer School, send a CV that includes a short
description of your educational background and one letter of
reference, unless you have already been granted a Ph.D. Please include
your name, address and current academic status.
Send all registration materials to All
registration materials should be delivered to the program by April
11, 2008. Materials received after the closing date will be evaluated
on a space available basis. Non U.S. citizens should begin immediately
to obtain travel documents.

The school will provide on-campus housing and meals. To share a room
with another student attending the school, the cost is $495 (USD) per
person. Housing rates are based on check-in Tuesday, July 22 and
check-out before noon on Thursday, July 31. Some single rooms may be
available for an additional fee of $150 (USD). If you'd like a single
room, please indicate your choice and we will try to accommodate you
on a first-come/first-served basis.

~~~~~~~~~~ Organizing committee: Matthew Fluet and Yannis Smaragdakis
Sponsors: National Science Foundation, ACM SIGPLAN, Microsoft Research

BDDs in ocaml


sasha mal asked and Pietro Abate answered:
> I wonder whether anyone has a BDD (binary decision diagram)
> implementation in ocaml. Ocaml interfaces to external BDD
> implementations in other languages (like Cudd) are of no use to me.

have a look at this paper for a non-optimized bdd implementation from
Jean-Christophe Filliatre.

I don't know if the full source code is avalaible.  I wasn't able to
find it. It would be interesting to repeat their experiments and play
with it.
Jean-Christophe Filliâtre then added:
I wrote the code by that time, but I was too lazy to package it. 
Here it is: 
Berke Durak also answered:
There is one small BDD module written by Xavier Leroy for an experimental 
SAT-solver during the EDOS project: 
Olivier Michel also answered:
I once wrote in the 90s a (RO)BDD implementation in caml-light (the 
translation to Ocaml should not be a big deal though) for the 
development of the declarative data-parallel language 8,5. The sources 
(unfortunately with comments in French, but they are pretty much 
straightforward!) are available here: 

is there a Roman Numeral library


Ashish Agarwal asked and Dave Benjamin answered:
> Hi all. Does anyone have an OCaml libary for working with Roman Numerals?
> Probably easy to write but am hoping it already exists. Thank you.

This is by no means a complete library, but I translated some conversion functions here:

Xmlm 1.0.0


Bünzli Daniel announced:
A new version of Xmlm is available. It is incompatible with the
previous one. The callback interface was dropped in favour of a
streaming (pull) interface. The tree interface was dropped in
favour of a custom tree construction interface tightly integrated
with the streaming interface. This has the following advantages :

* The input and output processes become symmetric.
* Reclaim your recursion ! There no inversion of control, the client drives
 the parsing process.
* Makes it easy to create tag level parsers and use parser combinator
* Allows to use the custom tree api on specific parts of the
 document only.

You can get a feel of the new interface by looking at the examples at

Other significant changes are :

* Namespace support, all names are now expanded names (attributes pertaining
 to namespaces are preserved in the result).
* Whitespace stripping respects the xml:space attribute.
* Xmlm is functorized on string and internal buffer types. Among
 other things this can be used to perform hash-consing, to
 overcome caml string limitations or to process the character
 stream, e.g. to normalize unicode characters or to convert to a
 custom encoding.
* UTF-8 documents can start with an UTF-8 encoded BOM.
* The file test/ couples each XHTML character entity with
 its corresponding UTF-8 encoded character string. You can use
 it to program a suitable entity callback to parse xhtml.

(New) project homepage :

As always, your (possibly negative yet constructive) feedback is welcome.

Using folding to read the cwn in vim 6+

Here is a quick trick to help you read this CWN if you are viewing it using vim (version 6 or greater).

:set foldmethod=expr
:set foldexpr=getline(v:lnum)=~'^=\\{78}$'?'<1':1

If you know of a better way, please let me know.

Old cwn

If you happen to miss a CWN, you can send me a message and I'll mail it to you, or go take a look at the archive or the RSS feed of the archives.

If you also wish to receive it every week by mail, you may subscribe online.

Alan Schmitt