Maurizio Proietti | 17 Apr 12:31 2014

LOPSTR 2014: Second Call for Papers

================== SECOND CALL FOR PAPERS ==================

                24th International Symposium on
       Logic-Based Program Synthesis and Transformation
                         LOPSTR 2014

  University of Kent, Canterbury, UK, September 10-11, 2014

Abstract submission:                     May 30, 2014
Paper/Extended abstract submission:      June 6, 2014


The aim of the LOPSTR series is to stimulate and promote international
research and collaboration on logic-based program development. LOPSTR
is open to contributions in logic-based program development in any
language paradigm. LOPSTR has a reputation for being a lively,
friendly forum for presenting and discussing work in progress. Formal
proceedings are produced only after the symposium so that authors can
incorporate this feedback in the published papers.

The 24th International Symposium on Logic-based Program Synthesis and
Transformation (LOPSTR 2014) will be held at the University of Kent,
Canterbury, United Kingdom; previous symposia were held in Madrid,
Leuven, Odense, Hagenberg, Coimbra, Valencia, Lyngby, Venice, London,
Verona, Uppsala, Madrid, Paphos, London, Venice, Manchester, Leuven,
Stockholm, Arnhem, Pisa, Louvain-la-Neuve, and Manchester.
LOPSTR 2014 will be co-located with PPDP 2014 (International ACM SIGPLAN
(Continue reading)

Raphael Bauduin | 17 Apr 11:37 2014

Beginner's troubles with ocsigen


I'm a beginner Ocaml developer, and wanted to start experimenting with Ocsigen. However, I have troubles preventing me to run even the simplest example...
I have installed eliom 3.0.3, js_of_ocaml 1.4.0 and all needed packages with opam (running ocaml 4.01.0).
I'm trying the examples at

./ page results in an error, of which this is an excerpt:

eliomc -infer  example.eliom
eliomc -c -noinfer  example.eliom
ocamlc.opt: unknown option `-noinfer'.

Trying the instructions at I get :

js_of_eliom -o example.js example.eliom
Missing primitives:

This is referenced here:
But this is some months old and would think the packages I installed with opam would work.

Anyone having suggestions?



PS: if there is an ocsigen mailing list, I'll gladly switch the discussion over there, but I didn't find any on the website.
Goswin von Brederlow | 17 Apr 10:52 2014

How does the Thread module work with the Gc?


as mentioned before I'm porting ocaml to run baremetal on a Raspberry
Pi and I'm getting close to a first release. Maybe porting is the
wrong word. I'm writing an exo kernel that you link to the ocamlopt
output to create a bootable kernel image. So just a verry thin layer
between hardware and ocaml.

What I'm currently a bit stuck with is the threading support and
interrupts. Since I don't plan to implement the pthread interface I
have to write my own Thread module. But it is verry similar to
otherlibs/systhread/ by necessity.

There seems to be 3 parts where the Thread module interacts with the Gc:

1) scan_roots_hook

This handles the per thread local roots, stacks and gc registers. This
ensures that data seen by any thread remains alive. Otherwise only
data seen by the current thread would be seen by the Gc.

2) stack usage estimation

No idea what that is for. It seems to add up the stack usage per

3) enter/leave_blocking_section

There is a mutex that prevents any two threads from leaving the
blocking section. I.e. no two threads can ever run ocaml code.

This is where the thread switching happens in the Thread module. This
causes threads to switch when you call e.g. Printf.printf.

But here is where my problem starts:

How does ocaml switch threads when a signal occurs? What if a thread
never enters a blocking section? Isn't there some other point where
tasks can be switched other than enter/leave_blocking_section?

I looked at the implementation for signals and they seem to set the
allocation limit for the thread to 0 so the next allocation will
trigger a Gc run. But how does that lead to a thread switch? What am I
missing here?



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

Michael Sperber | 17 Apr 09:23 2014

2nd CFP: FARM 2014: Functional Art, Music, Modelling and Design

If you are using OCaml or any mostly functional language in any
kind of musical, artistic, or design endeavour, please consider
contributing to FARM 2014, the 2nd ACM SIGPLAN International Workshop
of Functional Art, Music, Modelling and Design, co-located with ICFP

Find attached the Call for Papers and Demo Proposals.



			 FARM 2014

	 2nd ACM SIGPLAN International Workshop on
	Functional Art, Music, Modelling and Design

	   Gothenburg, Sweden; 6 September, 2014


The ACM SIGPLAN International Workshop on Functional Art, Music,
Modelling and Design (FARM) gathers together people who are harnessing
functional techniques in the pursuit of creativity and expression.

Functional Programming has emerged as a mainstream software
development paradigm, and its artistic and creative use is booming. A
growing number of software toolkits, frameworks and environments for
art, music and design now employ functional programming languages and
techniques. FARM is a forum for exploration and critical evaluation of
these developments, for example to consider potential benefits of
greater consistency, tersity, and closer mapping to a problem domain.

FARM encourages submissions from across art, craft and design,
including textiles, visual art, music, 3D sculpture, animation, GUIs,
video games, 3D printing and architectural models, choreography,
poetry, and even VLSI layouts, GPU configurations, or mechanical
engineering designs. The language used need not be purely functional
("mostly functional" is fine), and may be manifested as a domain
specific language or tool. Theoretical foundations, language design,
implementation issues, and applications in industry or the arts are
all within the scope of the workshop.

Submissions are invited in two categories:

  * Full papers

    5 to 12 pages using the ACM SIGPLAN template. FARM 2014
    is an interdisciplinary conference, so a wide range of
    approaches are encouraged and we recognize that the
    appropriate length of a paper may vary considerably
    depending on the approach. However, all submissions must
    propose an original contribution to the FARM theme, cite
    relevant previous work, and apply appropriate research

  * Demo abstracts

    Demo abstracts should describe the demonstration and its
    context, connecting it with the themes of FARM. A demo
    could be in the form of a short (10-20 minute) tutorial,
    presentation of work-in-progress, an exhibition of some
    work, or even a performance. Abstracts should be no
    longer than 2 pages, using the ACM SIGPLAN template and
    will be subject to a light-touch peer review.

If you have any questions about what type of contributions
that might be suitable, or anything else regarding
submission or the workshop itself, please contact the
organisers at:

    workshop2014 <at>


    Abstract (for Full Papers) submission deadline:	7 May
    Full Paper and Demo Abstract submission Deadline:	11 May
    Author Notification:				30 May
    Camera Ready:					18 June
    Workshop:						6 September


All papers and demo abstracts must be in portable document
format (PDF), using the ACM SIGPLAN style guidelines. The
text should be in a 9-point font in two columns. The
submission itself will be via EasyChair. See the FARM
website for further details:


Accepted papers will be included in the formal proceedings
published by ACM Press and will also be made available
through the the ACM Digital Library; see for information on the
options available to authors. Authors are encouraged to
submit auxiliary material for publication along with their
paper (source code, data, videos, images, etc.); authors
retain all rights to the auxiliary material.


Workshop Chair: Alex McLean, University of Leeds

Program Chair: Henrik Nilsson, University of Nottingham

Publicity Chair: Michael Sperber, Active Group GmbH

Program Committee:
Sam Aaron, Cambridge University
David Duke, University of Leeds
Kathleen Fisher, Tufts University
Julie Greensmith, University of Nottingham
Bas de Haas, Universiteit Utrecht
Paul Hudak, Yale University
David Janin, Université de Bordeaux
Richard Lewis, Goldsmiths, University of London
Louis Mandel, Collège de France
Alex McLean, University of Leeds
Carin Meier, Neo Innovation Inc
Rob Myers, Furtherfield
Henrik Nilsson, University of Nottingham (chair)
Dan Piponi, Google Inc
Andrew Sorensen, Queensland University of Technology
Michael Sperber, Active Group GmbH

For further details, see the FARM website:


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

Hugo Herbelin | 17 Apr 09:25 2014

Types Meeting 2014 in Paris, 12 - 15 May: 2nd call for participation

                        Types Meeting 2014
                       Paris, 12-15 May 2014


                     2nd CALL FOR PARTICIPATION

The 20th Conference "Types for Proofs and Programs" will take place at
the Institut Henri Poincaré (IHP) in Paris, France, from 12 to 15 May
2014, continued by the post-conference workshop "Proof, Computation,
Complexity" overlapping TYPES on May 15 afternoon and on May 16. Types
is this year an event associated to the special IHP trimester on
Semantics of proofs and certified mathematics

Invited speakers are

* Thierry Coquand, University of Gothenburg, Sweden
  A cubical set model of type theory

* Xavier Leroy, Inria Paris-Rocquencourt, France
  Formal verification of a static analyzer: abstract interpretation in type theory

* Andy Pitts, University of Cambridge, UK
  Nominal sets and dependent type theory

The Types Meeting is a forum to present new and on-going work in all
aspects of type theory and its applications, especially in formalized
and computer assisted reasoning and computer programming. It works as
a conference in our traditional workshop style and, this year, 39
contributed talks have been selected by the program committee on the
basis of abstracts of up to two pages (see

Registration is open, with early rate only until ** April 19 **.


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

Roberto Di Cosmo | 16 Apr 19:13 2014

ANN: Opam Dependency Solving in the Cloud

Dear all,
   we are quite happy to announce that Opam dependency solving in
now available in the Cloud, bringing the benefits of efficient
external dependency solvers to everybody.

With the steady growth in the number of Opam packages available,
the need for a fast, specialised and full fledged dependency solver
has started to surface : the internal heuristics may blow up [1]
and the default install/upgrade strategy may be unsatisfactory [2].

Since Opam builds on technology developed in Mancoosi [3] for solving
dependencies of GNU/Linux distributions, both of these issues can be easily
addressed by using one of the available external solvers: they will allow you to get
blazingly fast solving speed *and* offer an extensive preference language
designed to let you choose the install/upgrade strategy best suited for you [4]

How can you get an external solver? For Debian/Ubuntu users, it's just a matter
of typing "apt-get install aspcud", and that's it (really!). On other platforms,
things get hairy, though, to the point of discouraging many potential users.

Now to the good news: with the help of OcamlPro [5] and the Mancoosi team, we have
setup at Irill [6] a dependency solver farm that allows anybody on any platform
to access the latest external solvers in a breeze. 

This service has been already tested internally, and seems pretty fast and
stable, so we are now opening it up in beta test to the full Opam user community
in order to gather feedback, and nail down any remaining issue.

To use it, just follow the quite simple instructions provided here:

Happy dependency solving to all


[1] see for example
[2] see for example


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

Mitra Purandare | 16 Apr 14:49 2014

Second Call for Papers: International Conference on Formal Methods in Computer-Aided Design (FMCAD) 2014



International Conference on
Formal Methods in Computer-Aided Design (FMCAD)

Lausanne, Switzerland, October 21-24, 2014

The conference includes the FMCAD student forum;
it is collocated with MEMOCODE, DIFTS, and the
Hardware Model Checking Competition 2014 FMCAD Edition.

FMCAD 2014 has technical co-sponsorship from IEEE's CEDA
(Council on Electronic Design Automation) and
in-cooperation status with
ACM SIGPLAN (Special Interest Group on Programming Languages) and
ACM SIGSOFT (Special Interest Group on Software Engineering).


Abstract Submission: Tuesday, May 6
Paper Submission: Friday, May 16
Author Response Period: June 23-27
Author Notification: July 25
Camera-Ready Version: August 15
Conference: October 21-24


FMCAD 2014 is the 14th in a series of conferences on the
theory and application of formal methods in computer-aided
design and verification of computer systems and related
topics. FMCAD provides a leading international forum to
researchers and practitioners in academia and industry for
presenting and discussing novel methods, technologies,
theoretical results, tools, and open challenges in formal

FMCAD employs a rigorous peer-review process and is devoted
to maximizing the dissemination of papers.  Accepted papers
are distributed through both ACM and IEEE digital
libraries. In addition, published articles are made
available freely on the conference page and the authors
retain the copyright. There are no publication fees. At
least one of the authors is required to register for the
conference and present the accepted paper.

FMCAD 2014 will be co-located with MEMOCODE, the ACM/IEEE
International Conference on Formal Methods and Models for
Codesign, in Lausanne, Switzerland.  MEMOCODE will take
place from October 19 to 20, followed by a joint
FMCAD/MEMOCODE tutorial day on October 21.  FMCAD will
continue from October 22 to 24, 2014.


FMCAD welcomes submission of papers reporting original
research on advances in all aspects of formal methods
technology and its application to computer-aided design.
Topics of interest include, but are not limited to, the

-- Model checking, theorem proving, equivalence checking,
  abstraction and reduction, compositional methods,
  decision procedures at the bit- and word-level,
  probabilistic methods, combinations of deductive methods
  and decision procedures.

-- Synthesis and compilation for computer system
  descriptions, modeling, specification, and implementation
  languages, formal semantics of languages and their
  subsets, model-based design, design derivation and
  transformation, correct-by-construction methods.

-- Application of formal and semi-formal methods to
  functional and non-functional specification and
  validation of hardware and software, including timing and
  power modeling, verification of computing systems on all
  levels of abstraction, system-level design and
  verification for embedded and cyberphysical systems,
  hardware-software co-design and verification,
  transaction-level verification.

-- Experience with the application of formal and semi-formal
  methods to industrial-scale designs. Tools that represent
  formal verification enablement, new features, or a
  substantial improvement in the automation of formal

-- Application of formal methods in areas beyond computer
  systems, including formal methods describing processes
  studied in other areas of science, engineering, and


Submissions must be made electronically in PDF format
through a link available on the FMCAD web site

Two categories of papers can be submitted: regular papers (8
pages) and short papers (4 pages) containing ideas and
results that can be described succinctly.  Both regular and
short papers must use the IEEE Transactions format on
letter-size paper with a 10-point font size.

Submissions must contain original research that has not been
previously published, nor concurrently submitted for
publication. Any partial overlap with published or
concurrently submitted papers must be clearly indicated. If
experimental results are reported, authors are strongly
encouraged to provide adequate access to their data so that
results can be independently verified.

A small number of accepted papers will be considered for a
distinguished paper award. Recently awarded papers include:

* "An SMT Based Method for Optimizing Arithmetic
 Computations in Embedded Software Code", Hassan Eldib and
 Chao Wang (2013)

* "A quantifier-free SMT encoding of non-linear hybrid
 automata", Alessandro Cimatti, Sergio Mover and Stefano
 Tonetta (2012)

* "An Incremental Approach to Model Checking Progress Properties",
 Aaron Bradley, Fabio Somenzi, Zyad Hassan and Yan Zhang (2011)

* "Applying SMT in Symbolic Execution of Microcode", Anders
 Franzen, Alessandro Cimatti, Alexander Nadel, Roberto
 Sebastiani, and Jonathan Shalev (2010)


FMCAD 2014 will host a Student Forum that provides a
platform for graduate students at any career stage to
introduce their research to the wider Formal Methods
community, and solicit feedback. Submissions for the event
must be short reports describing research ideas or ongoing
work that the student is currently pursuing, and must be
within the scope of FMCAD.  Work, part of which has been
previously published, will be considered; the novel aspect
to be addressed in future work must be clearly described in
such cases.

The event will consist of short presentations by the student
authors of each accepted submission, and of a poster that
will be on display throughout the duration of the
conference.  Accepted submissions will be listed, with title
and author name, in the event description in the conference
proceedings.  The authors will also have the option to
upload their poster and presentation to the FMCAD web site.

Limited funds will be available for travel assistance for
students with accepted contributions.

More details are available at


Submission Deadline: Sunday, June 08
Acceptance notification: Sunday, Aug 03
Forum date: Monday, Oct 20


The following meetings will be co-located with this year's edition:

-- MEMOCODE 2014, the ACM/IEEE International Conference on
  Formal Methods and Models for Codesign
  ( )

-- DIFTS 2014, International Workshop on Design and
  Implementation of Formal Tools and Systems
  ( )

-- We are also proud to host this year's
  Hardware Model Checking Competition 2014 FMCAD Edition


Koen Claessen, Chalmers University of Technology
Viktor Kuncak, EPFL

Viktor Kuncak, EPFL

Barbara Jobstmann, EPFL, Jasper DA, and CNRS/Verimag

Ruzica Piskac, Yale University

Mitra Purandare, IBM Research Lab, Zurich


Jason Baumgartner, IBM
Dirk Beyer, University of Passau
Armin Biere, Johannes Kepler University
Per Bjesse, Synopsys
Nikolaj Bjorner, Microsoft Research
Roberto Bruttomesso, Atrenta
Gianpiero Cabodi, Politecnico di Torino
Hana Chockler, King's College
Alessandro Cimatti, FBK-irst
Koen Claessen (Chair), Chalmers University of Technology
Bruno Dutertre, SRI International
Ziyad Hanna, Jasper Design Automation
Keijo Heljanko, Aalto University
Alan Hu, University of British Columbia
Warren Hunt, University of Texas
Susmit Jha, Strategic CAD Lab, Intel
Daniel Kroening, University of Oxford
Viktor Kuncak (Chair), EPFL
Panagiotis Manolios, Northeastern University
Ken McMillan, Microsoft Research
Katell Morin-Allory, TIMA Laboratory, Grenoble
Lee Pike, Galois, Inc.
Ruzica Piskac, Yale University
Mitra Purandare, IBM Research Lab, Zurich
Sandip Ray, Intel Corporation
Philipp Ruemmer, Uppsala University
Andrey Rybalchenko, Microsoft Research Cambridge
Julien Schmaltz, TU Eindhoven
Natasha Sharygina, Universita' della Svizzera Italiana
Anna Slobodova, Centaur Technology
Niklas Sorensson, Chalmers University of Technology
Daryl Stewart, ARM
Cesare Tinelli, The University of Iowa
Martin Vechev, ETH Zurich
Thomas Wahl, Northeastern University
Georg Weissenbacher, Vienna University of Technology


Jason Baumgartner, IBM, USA
Armin Biere, Johannes Kepler University in Linz, Austria
Alan Hu, University of British Columbia, Canada
Warren Hunt, University of Texas at Austin, USA
Franck Cassez | 16 Apr 11:18 2014

ATVA 2014: Last Call for Papers -- Sydney November 3-7

[We apologise for duplicates.]
                   ATVA 2014 Call for Papers

          12th International Symposium on Automated
           Technology for Verification and Analysis

                   Sydney, November 3-7, 2014


Abstract submission:  NEW 19 April 2014
Paper submission:     NEW 27 April 2014

The purpose of ATVA is to promote research on theoretical and practical
aspects of automated analysis, verification and synthesis by providing
an international forum for interaction among the researchers in academia
and industry.

Abstract submission:  NEW 19 April 2014
Paper submission:     NEW 27 April 2014

Notification of acceptance:       30 June 2014
Final copy for proceedings:       30 July 2014
Conference:                       3-7 November 2014

ATVA 2014 solicits high quality submissions in areas related to the theory and
practice of automated analysis and verification of hardware and software systems.
Topics of interest include, but are not limited to:
Formalisms for modeling hardware, software and embedded systems
. Specification and verification of finite-state, infinite-state
and parameterized system
. Program analysis and software verification
. Analysis and verification of hardware circuits, systems-on-chip
and embedded systems
. Analysis of real-time, hybrid, timed, priced/weighted and probabilistic systems
. Deductive, algorithmic, compositional, and abstraction/refinement techniques
for analysis and verification
. Analytical techniques for safety, security, and dependability
. Testing and runtime analysis based on verification technology
. Synthesis and Games
. Analysis and verification of parallel and concurrent hardware/software systems
. Verification in industrial practice
. Applications and case studies
Theory papers should preferably be motivated by practical problems, and
applications should be based on sound theory and should solve problems of
practical interest.

ATVA invites research contributions in two categories: Regular research
papers (with 15 pages page limit) and tool papers (with 4 pages page limit).
Contributions must be written in English and in LNCS format, and must
present original research which is unpublished and not submitted elsewhere
(conferences or journals). The proceedings of ATVA 2014 will be
be published by Springer as a volume in the series of Lecture Notes in
Computer Science (LNCS). A special journal issue is also being planned
for selected papers.

  Pr. Krishnendu Chatterjee, IST Austria, Austria
  Pr. Ahmed Bouajjani, Univ. Paris Diderot, France

General Chair:
   Dr. Ralf Huuck (NICTA and UNSW)

Program co-chairs:
   Dr. Franck Cassez (NICTA and UNSW)
   Pr. Jean-François Raskin (ULB)

Workshop Chair:
   Dr. Peter Höefner (NICTA and UNSW)

Program committee:
   Ahmed Bouajjani (LIAFA, University Paris Diderot, France)
   Supratik Chakraborty (IIT Bombay, India)
   Alessandro Cimatti (FBK-irst, Italy)
   Deepak D'Souza (Indian Institute of Science, Bangalore, India)
   Hung Dang Van (UET, Vietnam National University, Hanoi)
   Giorgio Delzanno (DIBRIS, Università di Genova)
   E. Allen Emerson (The University of Texas at Austin, USA)
   Pierre Ganty (IMDEA Software Institute, Spain)
   Patrice Godefroid (Microsoft Research, USA)
   Kim Guldstrand Larsen (Aalborg University, Denmark)
   Teruo Higashino (Osaka University, Japan)
   Alan Hu (University of British Columbia, Canada)
   Joost-Pieter Katoen (RWTH Aachen University, Germany)
   Moonzoo Kim (KAIST, Korea)
   Gerwin Klein (NICTA and UNSW, Australia)
   Orna Kupferman (Hebrew University, Israel)
   Marta Kwiatkowska (University of Oxford, UK)
   Insup Lee (University of Pennsylvania, USA)
   Oded Maler (CNRS-VERIMAG, France)
   Annabelle McIver (Macquarie University, Australia)
   Madhavan Mukund (Chennai Mathematical Institute, India)
   Mizuhito Ogawa (Japan Advanced Institute of Science and Technology, Japan)
   Sungwoo Park Pohang (University of Science and Technology, Korea)
   Doron Peled (Bar Ilan University, Israel)
   Andreas Podelski (University of Freiburg, Germany)
   Pierre-Alain Reynier (Aix-Marseille University, France)
   Jie-Hong Rolland-Jiang (National Taiwan University Taipei, Taiwan)
   Jing Sun (The University of Auckland, New Zealand)
   P.S. Thiagarajan (National University of Singapore, Singapore)
   Ron Van Der Meyden (UNSW, Australia)
   Rob Van Glabbeek (NICTA and UNSW, Australia)
   Farn Wang (National Taiwan University Taipei, Taiwan)
   Chao Wang (Virginia Tech., USA)
   Bow-Yaw Wang (Academia Sinica, Taipei, Taiwan)
   Karsten Wolf (Rostock University, Germany)
   Hsu-Chun (Yen National Taiwan University, Taiwan)
   Wang Yi (Uppsala University, Sweden)
   Wenhui Zhang (Institute of Software, Chinese Academy of Sciences, China)

Steering Committee:
    Professor E. Allen Emerson (University of Texas at Austin)
    Professor Teruo Higashino (Osaka University)
    Professor Insup Lee (University of Pennsylvania)
    Professor Doron A. Peled (Bar Ilan Universioty)
    Professor Farn Wang (National Taiwan University)
    Professor Hsu-Chun Yen (National Taiwan University)


The information in this e-mail may be confidential and subject to legal professional privilege and/or
copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.


Caml-list mailing list.  Subscription management and archives:
Beginner's list:
Bug reports:
Paul-Andre Mellies | 16 Apr 10:11 2014

IHP thematic trimester -- Kick-off meeting -- Tuesday April 22

Dear all,

We are glad to announce the kick-off meeting of the thematic trimester 
** Semantics of proofs and certified mathematics **
which will be held at Institut Henri Poincaré (IHP), Paris, on the afternoon of Tuesday, April 22, 2014.

Four keynote speakers are invited to give a talk on this occasion:

• Georges Gonthier (Microsoft Research, Cambridge, and Microsoft INRIA Joint Center, Palaiseau)
Digitizing the Group Theory of the Odd Order Theorem
• Thomas Hales (University of Pittsburgh)
Formalizing the proof of the Kepler Conjecture
• Xavier Leroy (INRIA Paris-Rocquencourt)
Proof assistants in computer science research
• Vladimir Voevodsky (Institute for Advanced Study, Princeton)
Univalent Foundations - new type-theoretic foundations of mathematics

More information on the thematic trimester will be found on the webpage

You will find preliminary lists of confirmed invited speakers for the 5 workshops of the IHP programme

5–9 May         Workshop 1 Formalization of mathematics in proof assistants  
2–6 June         Workshop 2 Constructive mathematics and models of type theory
10–14 June Workshop 3 Semantics of proofs and programs
23–27 June Workshop 4 Abstraction and verification in semantics
7–11 July         Workshop 5 Certification of high-level and low-level programs

Registration to individual workshops is free but mandatory here:
(you do not need to register to the trimester unless you intend to stay for longer than the duration of a workshop)

The organisers
Pierre-Louis Curien <curien <at>>
Hugo Herbelin <Hugo.Herbelin <at>>
Paul-Andre Mellies <mellies <at>>

malc | 15 Apr 16:50 2014

[ANNOUNCE] llpp v18


New version of llpp (tagged v18) is now available at


llpp a graphical PDF viewer which aims to superficially resemble


* Bugfixes
* Synced with mupdf 1.4
* A lot of small usability tweaks
* Semblance of documentation at
  (Big thanks to Daan van Rossum)

mailto:av1474 <at>


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

Richard W.M. Jones | 15 Apr 16:34 2014

ppc64le backend

In case anyone is interested, Michel Normand wrote, and Fedora is
testing, a ppc64le backend for OCaml.

This might also be a good time to remind readers that Fedora is using
a fixed[1] arm64 backend written by Benedikt Meurer, and a ppc64 [big
endian] backend written by David Woodhouse plus some fixes by me.

All of these are available here:


[1] The fixes are for:
plus updated config.guess/config.sub from FSF:

Richard Jones
Red Hat


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