Peter Zotov | 23 Jul 11:55 2014

[ANN] ppx_deriving 0.1


I'm glad to announce an initial release of ppx_deriving,
a modular syntax extension for type-driven code generation.
It will be shortly available in OPAM.

I will introduce ppx_deriving with an example:

# #require "ppx_deriving";;
# type file = {
   kind : [ `File | `Dir ];
   name : string;
   perm : int [ <at> printer fun fmt -> Format.fprintf fmt "0o%03o"];
} [ <at>  <at> deriving Show, Eq];;
type file = { kind : [ `Dir | `File ]; name : bytes; perm : int; }
val pp_file : Format.formatter -> file -> unit = <fun>
val show_file : file -> bytes = <fun>
val equal_file : file -> file -> bool = <fun>
# print_endline (show_file { kind = `Dir; name = "bin"; perm = 0o755 
{ kind = `Dir; name = "bin"; perm = 0o755 }
- : unit = ()

A more thorough description is available in README[1].

While I intend this release to primarily serve as a preview for
the community and a means to gather feedback, it is fully usable
and documented. Some of the planned features (marked "TBD" in README)
are not yet implemented.

(Continue reading)

Oliver Bandel | 23 Jul 01:45 2014

lablgtk with OCamlMakefile


how can I convince OCamlMakefile to add the needed gtkInit-file to my program?

I tried around alot of things, looked up old answers on this list and  
at other places too,
also asked on irc.

No solution found.

Is it possible to solve this problem?
If so: how?



Caml-list mailing list.  Subscription management and archives:
Beginner's list:
Bug reports:

Martin Steffen | 15 Jul 13:22 2014

CFP FM2015 (20th Intl. Symposium on Formal Methods); 22.-26. June, 2015, Oslo

--------------------------=== FM 2015 ===----------------------------

       20th International Symposium on Formal Methods

                     Oslo, Norway, June 22-26, 2015


                                  Call for Papers



 Jan 2      Abstract submission deadline
 Jan 9      Full paper submission deadline
 March 23   Notification
 June 22-26 Conference



FM 2015 is the twentieth in a series of symposia organized by Formal 
 Methods Europe, an independent association whose aim is to stimulate 
 the use of, and research on, formal methods for software development. 
 The symposia have been notably successful in bringing together innovators 
 and practitioners in precise mathematical methods for software and systems 
 development, industrial users, as well as researchers. The FM symposia 
(Continue reading)

Phan Cong Vinh | 19 Jul 06:47 2014

ICTCC 2014: International Conference on NaTure of Computation and Communication (ICTCC) . Deadline: 31 July 2014

ICTCC 2014: International Conference on NaTure of Computation and
Communication (ICTCC)

- Submission Deadline: 31 July 2014
- Location: Ho Chi Minh City, Vietnam
- Website:

The ICTCC 2014 jointly organized by EAI and Nguyen Tat Thanh
University (NTTU) is a place for highly original ideas about how the
nature is going to shape computing systems of the future. Hence, it
focuses on rigorous approaches and cutting-edge solutions, which
encompass three classes of major methods:

Those that take inspiration from nature for the development of novel
problem solving techniques;
Those that are based on the use of computers or networks to synthesize
natural phenomena; and
Those that employ natural materials (e.g., molecules,) to compute or

Its purpose is to make a formal basis more accessible to researchers,
scientists, professionals and students as well as developers and
practitioners in ICT by providing them with state-of-the-art research
results, applications, opportunities and future trends.

We hope that the conference will receive many papers and the
participation of a large number of students, researchers, and
professionals from all over the world.
(Continue reading)

BigDat 2015: 23 July registration deadline

*To be removed from our mailing list, please respond to this message with UNSUBSCRIBE in the subject line*



BigDat 2015

Tarragona, Spain

January 26-30, 2015

Organized by
Rovira i Virgili University


--- 2nd registration deadline: July 23, 2014 ---



BigDat 2015 is a research training event for graduates and postgraduates in the first steps of their
academic career. It aims at updating them about the most recent developments in the fast developing area
of big data, which covers a large spectrum of current exciting research, development and innovation with
an extraordinary potential for a huge impact on scientific discoveries, medicine, engineering,
business models, and society itself. Renowned academics and industry pioneers will lecture and share
(Continue reading)

Yoriyuki Yamagata | 18 Jul 16:08 2014

A proposal of a standard support for Unicode string

Dear List,

I write a blog post which proposes inclusion of Unicode strings in OCaml standard distribution.

The reason for this proposal can be summarized as follows.

  1. Type for human readable text is too important to left out from the standard distribution, in particular from the beginner's perspective

  2. This enhances interpolability of Unicode processing libraries

  3. This suppresses the current dangerous practice that raw UTF-8 encoded string is used for Unicode string.

I hope this stimulates the further discussion of human readable texts in OCaml

Yoriyuki Yamagata
Hugo Herbelin | 18 Jul 15:45 2014

CFP Post-proceedings TYPES 2014 Types for Proofs and Programs (open call)

Call for papers: Types for Proofs and Programs,
  post-proceedings of TYPES 2014 (open call)

TYPES is a major forum for the presentation of research on all aspects
of type theory and its applications. The post-proceedings of TYPES
2014, which was held May 12-15 in Paris, are open to everyone, also
those who did not participate in the conference. We would like to
invite all researchers that study type systems to share their results
concerning type-based theorem proving environments or type-based
formal modelling, in particular we welcome submissions on any topic in
the following list:

 - Foundations of type theory and constructive mathematics
 - Applications of type theory
 - Dependently-typed programming
 - Industrial uses of type theory technology
 - Meta-theoretic studies of type systems
 - Proof-assistants and proof technology
 - Automation in computer-assisted reasoning
 - Links between type theory and functional programming
 - Formalising mathematics using type theory. 

Important dates

Abstract submission deadline:   1 September 2014
Paper submission deadline:      8 September 2014
Notification of acceptance:    15 February  2015


* Papers must be submitted in PDF format using EasyChair:

* Authors have the option to include an attachment (.zip or .tgz)
  containing mechanised proofs, but reviewers are not obliged to take
  these attachments into account. Attachments will not be published.

* The post-proceedings will be published in LIPIcs (Leibniz
  International Proceedings in Informatics,
  ""), an open-access
  series of conference proceedings. Incidentally, publication of TYPES
  2013 post-proceedings is imminent as volume 26 of the LIPIcs series

* We recommend to keep the length of the contributions in the range of
  15-25 pages, and 25 pages is the upper limit for the submissions.


Hugo Herbelin           Inria Paris-Rocquencourt, France
Pierre Letouzey         University Paris-Diderot, France
Matthieu Sozeau         Inria Paris-Rocquencourt, France


Caml-list mailing list.  Subscription management and archives:
Beginner's list:
Bug reports:

Kakadu | 17 Jul 12:37 2014

Lablqt 0.3 is out

Hi all!

Lablqt will help you to create GUI applications with using QtQuick 2
and OCaml. It includes PPX syntax extension and ocamlfind package.
It's available in OPAM already.

Tutorial: .

Kind regards,
Dmitrii Kosarev a.k.a. Kakadu

P.S. Many thanks to guys who helped me in improving of the tutorial.


Caml-list mailing list.  Subscription management and archives:
Beginner's list:
Bug reports:

Klaus Havelund | 17 Jul 08:25 2014

[fm-announcements] Call for Papers: NASA Formal Methods (NFM) 2015


The 7th NASA Formal Methods Symposium

27 - 29 April 2015
Pasadena, California, USA


The widespread use and increasing complexity of mission- and safety-critical systems require advanced techniques that address their specification, verification, validation, and certification.

The NASA Formal Methods Symposium is a forum for theoreticians and practitioners from academia, industry, and government, with the goals of identifying challenges and providing solutions to achieving assurance in mission- and safety-critical systems. Within NASA such systems include for example autonomous robots, separation assurance algorithms for aircraft, Next Generation Air Transportation (NextGen), and autonomous rendezvous and docking for spacecraft. Moreover, emerging paradigms such as property-based design, code generation, and safety cases are bringing with them new challenges and opportunities. The focus of the symposium will be on formal techniques, their theory, current capabilities, and limitations, as well as their application to aerospace, robotics, and other mission- and safety-critical systems in all design life-cycle stages. We encourage submissions on cross-cutting approaches marrying formal verification techniques with advances in critical system development, such as requirements generation, analysis of aerospace operational concepts, and formal methods integrated in early design stages and carrying throughout system development.


Topics of interest include, but are not limited to:

  • Model checking
  • Theorem proving
  • SAT and SMT solving
  • Symbolic execution
  • Static analysis
  • Runtime verification
  • Program refinement
  • Compositional verification
  • Modeling and specification formalisms
  • Model-based development
  • Model-based testing
  • Requirement engineering
  • Formal approaches to fault tolerance
  • Security and intrusion detection
  • Applications of formal methods to aerospace systems
  • Applications of formal methods to cyber-physical systems
  • Applications of formal methods to human-machine interaction analysis


Paper Submission: 10 Nov 2014
Paper Notifications: 12 Jan 2015
Camera-ready Papers: 9 Feb 2015
Symposium: 27 - 29 April 2015


The symposium will take place at the Hilton Hotel, Pasadena, California, USA, April 27-29, 2015.

There will be no registration fee for participants. All interested individuals, including non-US citizens, are welcome to submit, to attend, to listen to the talks, and to participate in discussions; however, all attendees must register.


There are two categories of submissions:

  1. Regular papers describing fully developed work and complete results (15 pages)
  2. Short papers describing tools, experience reports, or descriptions of work in progress with preliminary results (6 pages)

All papers should be in English and describe original work that has not been published or submitted elsewhere. All submissions will be fully reviewed by members of the Programme Committee. Papers will appear in a volume of Springer's Lecture Notes on Computer Science (LNCS), and must use LNCS style formatting. Papers should be submitted in PDF format.


Klaus Havelund, NASA Jet Propulsion Laboratory
Gerard Holzmann, NASA Jet Propulsion Laboratory
Rajeev Joshi, NASA Jet Propulsion Laboratory


Erika Abraham, RWTH Aachen University, Germany
Julia Badger, NASA Johnson Space Center, USA
Christel Baier, Technische Universität Dresden, Germany
Saddek Bensalem, VERIMAG/UJF, France
Dirk Beyer, University of Passau, Germany
Armin Biere, Johannes Kepler University, Austria
Nikolaj Bjorner, Microsoft Research, USA
Borzoo Bonakdarpour, McMaster University, Canada
Alessandro Cimatti, Fondazione Bruno Kessler, Italy
Leonardo de Moura, Microsoft Research, USA
Ewen Denney, NASA Ames Research Center, USA
Ben Di Vito, NASA Langley Research Center, USA
Dawson Engler, Stanford University, USA
Jean-Christophe Filliatre, Université Paris-Sud, France
Dimitra Giannakopoulou, NASA Ames Research Center, USA
Alwyn Goodloe, NASA Langley Research Center, USA
Alex Groce, Oregon State University, USA
Radu Grosu, Vienna University of Technology, Austria
John Harrison, Intel Corporation, USA
Mike Hinchey, University of Limerick/Lero, Ireland
Bart Jacobs, University of Leuven, Belgium
Sarfraz Khurshid, The University of Texas at Austin, USA
Gerwin Klein, NICTA, Australia
Daniel Kroening, Oxford University, UK
Orna Kupferman, Hebrew University Jerusalem, Israel
Kim Larsen, Aalborg University, Denmark
Rustan Leino, Microsoft Research, USA
Martin Leucker, University of Lubeck, Germany
Rupak Majumdar, Max Planck Institute, Germany
Pete Manolios, Northeastern University, USA
Peter Mueller, ETH Zurich, Switzerland
Kedar Namjoshi, Bell Labs/Alcatel-Lucent, USA
Corina Pasareanu, NASA Ames Research Center, USA
Doron Peled, Bar Ilan University, Israel
Suzette Person, NASA Langley Research Center, USA
Andreas Podelski, University of Freiburg, Germany
Grigore Rosu, University of Illinois, USA
Kristin Rozier, NASA Ames Research Center, USA
Natarajan Shankar, SRI International, USA
Natasha Sharygina, University of Lugano, Switzerland
Scott Smolka, Stony Brook University, USA
Willem Visser, University of Stellenbosch, South Africa
Mahesh Viswanathan, University of Illinois, USA
Mike Whalen, University of Minnesota, USA
Jim Woodcock, University of York, UK


Julia Badger, NASA Johnson Space Center
Ewen Denney, NASA Ames Research Center
Ben Di Vito, NASA Langley Research Center
Klaus Havelund, NASA Jet Propulsion Laboratory
Gerard Holzmann, NASA Jet Propulsion Laboratory
Cesar Munoz, NASA Langley Research Center
Corina Pasareanu, NASA Ames Research Center
Suzette Person, NASA Langley Research Center
Kristin Y. Rozier, NASA Ames Research Center

To opt-out from this mailing list, send an email to

fm-announcements-request <at>

with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting

fm-announcements-owner <at> 
Oliver Bandel | 17 Jul 02:31 2014

Article on why they use Ocaml: "Why We Use OCaml | Esper Tech Blog"

Just found this via ycombinator:



Caml-list mailing list.  Subscription management and archives:
Beginner's list:
Bug reports:

Alain Frisch | 15 Jul 17:26 2014

Existential row types

Dear all,

GADTs allow to restrict existential type variables to being an instance 
of a row type, as in:

class type c = ...

type s =
   | EX: ((#c as 'a) -> unit) * (unit -> 'a) -> ex

I'm wondering if it is possible to simulate such restricted existential 
quantification with first-class module and private row types.  Something 

module type S = sig
   type t = private #c
   val f: t -> unit
   val g: unit -> t

let foo (type t_) (f : (#c as t_) -> unit) (g : unit -> t_) =
   let module M = struct
     type t = t_
     let f = f
     let g = g
   (module M : S)

This does not work, of course, because of the "... as t_".  Is there a 
local work-around?  If not, I'm wondering if if would be easy (and make 
sense) to introduce a form for introducing locally private row types:

  let foo (type t_ = private #c) (f : t_ -> unit) (g : unit -> t_) = ...

-- Alain


Caml-list mailing list.  Subscription management and archives:
Beginner's list:
Bug reports: