• en

# OCaml Planet

The OCaml Planet aggregates various blogs from the OCaml community. If you would like to be added, read the Planet syndication HOWTO.

# CUFP 2014 Call for Presentations — CUFP, Apr 20, 2014

CUFP 2014 will be held in Gothenburg, Sweden.

read more

# Coq received ACM Software System 2013 award — Coq, Apr 19, 2014

After the ACM SIGPLAN Programming Languages Sofware 2013 Award, Coq received the ACM Software System 2013 award.

read more

# Typeful disjunctive normal form — Matthias Puech, Apr 18, 2014

This is the answer to last post’s puzzle. I gave an algorithm to put a formula in disjunctive normal form, and suggested to prove it correct in OCaml, thanks to GADTs. My solution happens to include a wealth of little exercises that could be reused I think, so here it is.

I put the code snippets in the order that I think is more pedagogical, and leave to the reader to reorganize them in the right one.

First, as I hinted previously, we are annotating formulas, conjunctions and disjunctions wit…

# The 6 parameters of (’a, ’b, ’c, ’d, ’e, ’f) format6 — GaGallium, Apr 18, 2014

The infamous `format6` type is the basis of the hackish but damn convenient, type-safe way in which OCaml handles format strings:

``````Printf.printf "%d) %s -> %f\n"
3 "foo" 5.12
``````

The first argument of `printf` in this example is not a string, but a format string (they share the same literal syntax, but have different type, and there is a small hack in the type-inference engine to make this possible). It's type, which you can get by asking `("%d) %s -> %f\n" : (_,_,_,_,_,_) format6)` in a topleve…

# Disjunctive normal forms in big steps — Matthias Puech, Apr 15, 2014

This is probably a second-semester functional programming exercise, but I found it surprisingly hard, and could not find a solution online. So at the risk of depriving a TA from a problem for its mid-term exam, here is my take on it, that I painfully put together yesterday.

Given a formula built out of conjunction, disjunction and atoms, return its disjunctive normal form, in big step or natural semantics, that is, not applying repetitively the distributivity and associativity rules, but in a si…

# OCamlPro Highlights: March 2014 — OCamlPro, Apr 15, 2014

Here is a short report of some of our activities in March 2014 !

## Welcome Thomas

First, we would like to welcome Thomas Blanc on board ! Thomas is starting a PhD at OCamlPro, with Michel Mauny from ENSTA as his PhD advisor. So, he will stay with us for three years, working on static analysis of whole OCaml programs, with two main objectives:

• To detect uncaught exceptions, using a different approach than `ocamlexc`, the tool that François Pessaux developed during his PhD thesis, a method that wi…

# Ocsigen Js_of_ocaml 2.0 — Ocsigen project, Apr 11, 2014

We are happy to announce release 2.0 of Js_of_ocaml, the compiler from OCaml bytecode to JavaScript.

A lot of efforts has been put in reducing the size of the generated JavaScript code. Much shorter variable names are used; unnecessary whitespaces and semicolons are omitted; multiple occurrences of a same constant are shared... The runtime is minified as well. You can expect a space reduction of 15% to 20%.

Recursive modules are now supported. Tail calls between mutually recursive functions …

# Inlined records in constructors — LexiFi, Apr 10, 2014

I'd like to introduce a new language feature, inlined record arguments on constructors, which I propose for inclusion in OCaml. In a nutshell, it allows you to define a record directly within a sum type constructor:

 ```1 2 3 ``` ```  type t =      | A of { x : int; y: string }      | ...```

The argument of the constructor is a full-fledged record type. All features of records are available: dot notation, mutable fields, polymorphic fields, punning syntax, record override. You ca…