Pierre-Alexandre Voye | 23 Apr 11:50 2014
Picon

Module inside an object

Hello,
I would like to define a parameterized module inside an object by the type of this object.


I have two module interlocked :

(* Parameters*)
module type A = sig
        type agent
        type intern_agent = { i : agent}
        val create : agent -> intern_agent
end

module type E = sig
        type event
end



module  type StateType = sig

  type agent
  type event

  type  state_t = { 
    mutable name : string;
    mutable parentstate  :  state_t option;
  }
end


module State (A : A) (E : E) = struct

        type agent = A.agent
        type event = E.event
    type  state_t = { 
            mutable name : string;
             mutable parentstate  :  state_t option;
    }


    (*...*)
end



module Agent (S : StateType) =
        struct
          type agent = S.agent
          type event = S.event
          type state_t = S.state_t

      type  agent_t = {
          mutable agent      : agent ;
      }

      let create a1   = {
          agent          = a1;
      }
end


(* An implementation of E*)
type event1 = Event1 | Event2;;
module E = struct type event = event1 end;;




What I would like to do is something like that (which is syntacticly incorrect but represents what I would like to do) :


class  character = object (self :'self)
 val mutable position        = (0,0)
 val agent                         =
                let A = (module Ag  = struct
                                type agent = 'self
                                type intern_agent = { i : agent}
                                let create a = { i = a }
                              end)
                     in
                let Ag = (module Agent(State(A)(E)) ) in
                Ag.create self
 
 method getPosition          = position
 
end;;

 

How can I write this to be able to define a value which is an Agent parametrized by itself ?

Thank you,

--
Evgenii Lepikhin | 23 Apr 10:26 2014
Picon

strange behavior of camlp4 + batteries

Hello,

I was unable to use Batteries inside camlp4 module. Short command line test:

$ camlp4o -I .../ocaml -I .../batteries -I .../num nums.cma bigarray.cma
batteries.cma

Camlp4: Uncaught exception: DynLoader.Error (".../batteries.cma", "error while
linking .../batteries.cma.\nThe external function `caml_ba_dim_3' is not
available")

Bigarray is installed correctly:
==========================
$ cat test.ml
open Bigarray

let () =
        let a = Array3.create float32 c_layout 10 10 10 in
        Printf.printf "dim3 = %i\n" (Array3.dim3 a)
==========================
$ ocamlbuild -use-ocamlfind test.native --
Finished, 4 targets (0 cached) in 00:00:00.
dim3 = 10
==========================

What's wrong?

--

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

Romain Bardou | 22 Apr 10:03 2014

Obj.magic for polymorphic identifiers

Hello,

I'm considering using Obj.magic and as the type-checker can no longer
ensure type safety, I decided to come here for advice.

I want to implement the trick with GADTs where you test equality of
unique identifiers, and if they match this adds an equality constraint
on types. I want this code to be small and well abstracted in a module
so that if this module is safe, then using this module cannot cause a
seg fault.

Here is the signature of my module:

(************************************************************************)
(** Polymorphic identifiers. *)

(** The type of identifiers associated to type ['a]. *)
type 'a t

(** Make a new, fresh identifier.
    This is the only way to obtain a value of type [t]. *)
val fresh: unit -> 'a t

(** Type constraint which is conditioned on identifier equality. *)
type (_, _) equal =
  | Equal: ('a, 'a) equal
  | Different: ('a, 'b) equal

(** Equality predicate. *)
val equal: 'a t -> 'b t -> ('a, 'b) equal

(** Convert an identifier to an integer.
    The integer is guaranteed to be unique for each call to {!fresh}. *)
val to_int: 'a t -> int
(************************************************************************)

and here is the implementation:

(************************************************************************)
type 'a t = int

let fresh =
  let counter = ref (-1) in
  fun () ->
    incr counter;
    !counter

type (_, _) equal =
  | Equal: ('a, 'a) equal
  | Different: ('a, 'b) equal

let equal (type a) (type b) (a: a t) (b: b t): (a, b) equal =
  if a = b then
    (Obj.magic (Equal: (a, a) equal): (a, b) equal)
  else
    Different

let to_int x =
  x
(************************************************************************)

Finally, here is a test program:

(************************************************************************)
open Polid

let () =

  let x = fresh () in
  let y = fresh () in

  let eq (type a) (type b) (t: a t) (u: b t) (a: a) (b: b) =
    match equal t u with
      | Equal ->
          if a = b then "true" else "false"
      | Different ->
          "false"
  in

  print_endline (eq x y 5 "salut"); (* false *)
  print_endline (eq x x 5 5); (* true *)
  print_endline (eq x x 5 9); (* false *)
  print_endline (eq y y "test" "salut"); (* false *)
  print_endline (eq y y "test" "test"); (* true *)
  print_endline (eq y x "salut" 5); (* false *)
  (* print_endline (eq x x 5 "salut"); (\* type error *\) *)
  (* print_endline (eq y y "salut" 5); (\* type error *\) *)

  ()
(************************************************************************)

It relies heavily on the fact that "fresh ()" cannot be generalized as
'a t is abstract.

A typical use case is as follows: I have two heterogeneous association
lists (using GADTs for existential types). As I iterate on one of those
lists, I need to find the corresponding item in the other list. As I
unpack the existential, the type-checker cannot prove that the
existential types are equal, hence the need for a runtime check (a call
to Polid.equal).

Can you find any reason why this would not be safe, or any better way to
implement this?

Thank you,

-- 
Romain Bardou
-- 
Romain Bardou
Cryptosense
96bis boulevard Raspail, 75006 Paris, France
+33 (0)9 72 42 35 31

--

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

Serge Autexier | 22 Apr 09:23 2014
Picon

CfP: 8th Verification Workshop (VERIFY 2014), Focus Theme: Verification Beyond IT Systems, extended deadline *May 5th, 2014*

[Apologies for cross posting, Deadline extended to *May 5th, 2014*]

                            CALL FOR PAPERS

         8th International Verification Workshop (VERIFY'14)
              in connection with IJCAR 2014 at FLoC 2014
                  July 23-24, 2014, Vienna, Austria

                       http://vsl2014.at/verify

The formal  verification of  critical information  systems has  a long
tradition  as one  of  the  main areas  of  application for  automated
theorem proving. Nevertheless, the area is of still growing importance
as the number of computers  affecting everyday life and the complexity
of  these systems  are  both  increasing. The  purpose  of the  VERIFY
workshop  series is  to  discuss problems  arising  during the  formal
modeling and  verification of  information systems and  to investigate
suitable solutions.  Possible perspectives include those  of automated
theorem proving, tool support, system engineering, and applications.

The VERIFY  workshop series aims  at bringing together people  who are
interested in the development of safety and security critical systems,
in formal  methods, in  the development  of automated  theorem proving
techniques,  and  in  the   development  of  tool  support.  Practical
experiences gained in  realistic verifications are of  interest to the
automated theorem proving community and new theorem proving techniques
should  be transferred  into practice.  The overall  objective of  the
VERIFY workshops is to identify  open problems and to discuss possible
solutions under the theme

What are the verification problems? What are the deduction techniques?

The 2014 edition of VERIFY aims for extending the verification methods
for processes implemented in hard-  and software to processes that may
well include computer-assistance, but have  a large part or a frequent
interaction  with non-computer-based  process  steps.  Hence the  2014
edition will run under the focus theme

                    Verification Beyond IT Systems

A  non-exclusive list of application areas  with these characteristics
are

       * Ambient assisted living
       * Intelligent home systems and processes
       * Business systems and processes
       * Production logistics systems and processes
       * Transportation logistics
       * Clinical processes
       * Social systems and processes (e.g., voting systems)

The scope of VERIFY includes topics such as

       * ATP techniques in verification
       * Case studies (specification & verification)
       * Combination of verification systems
       * Integration of ATPs and CASE-tools
       * Compositional & modular reasoning
       * Experience reports on using formal methods
       * Gaps between problems & techniques
       * Formal methods for fault tolerance
       * Information flow control security
       * Refinement & decomposition
       * Reliability of mobile computing
       * Reuse of specifications & proofs
       * Management of change
       * Safety-critical systems
       * Security models
       * Tool support for formal methods

Submissions are encouraged in one of the following two categories:

A. Regular  paper:  Submissions  in  this  category  should   describe
   previously unpublished  work (completed or in  progress), including
   descriptions of research, tools,  and applications.  Papers must be
   5-14  pages  long (in  EasyChair  style)  or  6-15 pages  long  (in
   Springer LNCS style).

B. Discussion  papers: Submissions  in this  category are  intended to
   initiate discussions and hence should address controversial issues,
   and may include  provocative statements. Papers must  be 3-14 pages
   long  (in EasyChair  style) or  3-15 pages  long (in  Springer LNCS
   style).

Important dates
   Abstract Submission Deadline:    May 5th, 2014 (extended)
   Paper Submission Deadline:       May 5th, 2014 (extended)
   Notification of acceptance:      May 20, 2014
   Final version due:               May 27, 2014
   Workshop date:                   July 23-24, 2014

Submission is via EasyChair:
   http://www.easychair.org/conferences/?conf=verify2014

Program Committee

 Serge Autexier (DFKI) - chair
 Bernhard Beckert (Karlsruhe Institute of Technology) - chair
 Wolfgang Ahrendt (Chalmers University of Technology)
 Juan Augusto (Middlesex University)
 Iliano Cervesato (Carnegie Mellon University)
 Jacques Fleuriot (University of Edinburgh)
 Marieke Huisman (University of Twente)
 Dieter Hutter (DFKI GmbH)
 Reiner Haehnle (Technical University of Darmstadt)
 Deepak Kapur (University of New Mexico)
 Gerwin Klein (NICTA and UNSW)
 Joe Leslie-Hurd (Intel Corporation)
 Fabio Martinelli (IIT-CNR)
 Catherine Meadows (NRL)
 Stephan Merz (INRIA Lorraine)
 Tobias Nipkow (TU Munich)
 Lawrence Paulson (University of Cambridge)
 Johann Schumann (SGT, Inc/NASA Ames)
 Kurt Stenzel (University of Augsburg)

--

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

Daniel Bünzli | 21 Apr 23:30 2014
Picon

non-optional labels in signatures

Hello,

This is certainly a question for Jacques Garrigue. I'm asking out of pure curiosity if there's a particular
reason why non-optional labels in signatures don't have the ~ ? Is to save a keystroke ? 

(I happen to make the error of putting them in signatures fairly often) 

Best, 

Daniel 

--

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

Maurizio Proietti | 17 Apr 12:31 2014
Picon

LOPSTR 2014: Second Call for Papers

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

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

           http://www.iasi.cnr.it/events/lopstr14/
  University of Kent, Canterbury, UK, September 10-11, 2014

DEADLINES
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
Symposium on Principles and Practice of Declarative Programming).

Topics of interest cover all aspects of logic-based program
development, all stages of the software life cycle, and issues of both
programming-in-the-small and programming-in-the-large. Both full
papers and extended abstracts describing applications in these areas
are especially welcome. Contributions are welcome on all aspects of
logic-based program development, including, but not limited to:

    * synthesis
    * transformation
    * specialization
    * composition
    * optimization
    * inversion
    * specification
    * analysis and verification
    * testing and certification
    * program and model manipulation
    * transformational techniques in SE
    * applications and tools

Survey papers that present some aspects of the above topics from a new
perspective, and application papers that describe experience with
industrial applications are also welcome.

Papers must describe original work, be written and presented in
English, and must not substantially overlap with papers that have been
published or that are simultaneously submitted to a journal,
conference, or workshop with refereed proceedings. Work that already
appeared in unpublished or informally published workshop proceedings
may be submitted (please contact the PC co-chairs in case of questions).

Important Dates

 Abstract submission:                            May 30, 2014
 Paper/Extended abstract submission:             June 6, 2014
 Notification:                                   July 18, 2014
 Camera-ready (for electronic pre-proceedings):  August 25, 2014
 Symposium:                                      September 10-11, 2014

Submission Guidelines

Authors should submit an electronic copy of the paper (written in English)
in PDF, formatted in the Lecture Notes in Computer Science style.
Each submission must include on its first page the paper title; authors
and their affiliations; contact author's email; abstract; and three to
four keywords which will be used to assist the PC in selecting appropriate
reviewers for the paper. Page numbers should appear on the manuscript to
help the reviewers in writing their report. Submissions cannot exceed 15
pages including references but excluding well-marked appendices not intended
for publication. Reviewers are not required to read the appendices, and thus
papers should be intelligible without them.
Paper should be submitted via the Easychair submission website for LOPSTR 2014.
If electronic submission is impossible, please contact the program co-chairs
for information on how to submit hard copies.

Proceedings

The formal post-conference proceedings will be published by Springer in the
Lecture Notes in Computer Science series. Full papers can be directly accepted
for publication in the formal proceedings, or accepted only for presentation at
the symposium and inclusion in informal proceedings. After the symposium, all
authors of extended abstracts and full papers accepted only for presentation
will be invited to revise and/or extend their submissions in the light of the
feedback solicited at the symposium. Then, after another round of reviewing,
these revised papers may also be published in the formal proceedings.

Program Committee

Slim Abdennadher        German University of Cairo, Egypt
Étienne André          Université Paris 13, France
Martin Brain            University of Oxford, UK
Wei-Ngan Chin        National University of Singapore, Singapore
Marco Comini            University of Udine, Italy
Wlodzimierz Drabent     IPIPAN, Poland and Linköping University, Sweden
Fabio Fioravanti        University of Chieti-Pescara, Italy
Jürgen Giesl        RWTH Aachen University, Germany
Miguel Gómez-Zamalloa Complutense University of Madrid, Spain
Arnaud Gotlieb        SIMULA Research Laboratory, Norway
Gopal Gupta             University of Texas at Dallas, USA
Jacob Howe              City University London, UK
Zhenjiang Hu        National Institute of Informatics, Japan
Alexei Lisitsa        University of Liverpool, UK
Yanhong Annie Liu       Stony Brook University, USA
Jorge Navas        NASA, USA
Naoki Nishida        Nagoya University, Japan
Corneliu Popeea         Technische Universität München, Germany
Maurizio Proietti       IASI-CNR, Italy (Program Co-Chair)
Tom Schrijvers        Ghent University, Belgium
Hirohisa Seki        Nagoya Institute of Technology, Japan (Program Co-Chair)
Jon Sneyers        K.U. Leuven, Belgium
Fausto Spoto        University of Verona, Italy
Wim Vanhoof             University of Namur, Belgium
German Vidal            Universitat Politecnica de Valencia, Spain

Program Co-Chairs:

Maurizio Proietti, IASI-CNR, Italy (maurizio.proietti <at> iasi.cnr.it)
Hirohisa Seki, Nagoya Institute of Technology, Japan (seki <at> nitech.ac.jp)

Symposium Co-Chairs

Olaf Chitil and Andy King
School of Computing
University of Kent
CT2 7NF Kent, UK

Organizing Committee

Emanuele De Angelis, University of Chieti-Pescara and IASI-CNR, Italy
Fabrizio Smith, IASI-CNR, Italy

============================================================

--

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
Raphael Bauduin | 17 Apr 11:37 2014
Picon

Beginner's troubles with ocsigen


Hi,

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 https://github.com/db0company/Ocsigen-Quick-Howto

./make.sh 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 http://ocsigen.org/eliom/manual/workflow-compilation I get :

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

This is referenced here: https://github.com/ocsigen/js_of_ocaml/issues/20
But this is some months old and would think the packages I installed with opam would work.

Anyone having suggestions?

Thanks

Raph

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
Picon

How does the Thread module work with the Gc?

Hi,

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
thread.

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?

MfG
	Goswin

--

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

Michael Sperber | 17 Apr 09:23 2014
Picon

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
2014.

Find attached the Call for Papers and Demo Proposals.

Regards,
Mike

--------------------------------------------------------------

			 FARM 2014

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

	   Gothenburg, Sweden; 6 September, 2014

                http://functional-art.org

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
    methods.

  * 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> functional-art.org

KEY DATES:

    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

SUBMISSION

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:

        http://functional-art.org

PUBLICATION

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
http://authors.acm.org/main.cfm 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 ORGANISATION

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:
        http://functional-art.org

--

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

Hugo Herbelin | 17 Apr 09:25 2014
Picon
Picon

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

                        Types Meeting 2014
                       Paris, 12-15 May 2014

           http://www.pps.univ-paris-diderot.fr/types2014

                     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
(https://ihp2014.pps.univ-paris-diderot.fr).

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
http://www.pps.univ-paris-diderot.fr/types2014/Program).

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

--

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

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:

    http://cudf-solvers.irill.org/index.html

Happy dependency solving to all

--
Roberto

[1] see for example https://github.com/ocaml/opam/issues/1056
    or https://github.com/ocaml/opam/issues/685
[2] see for example https://github.com/ocaml/opam/issues/1161
    or https://github.com/ocaml/opam/issues/1334
[3] http://www.mancoosi.org
[4] http://opam.ocaml.org/doc/Specifying_Solver_Preferences.html
[5] http://www.ocamlpro.com
[6] http://www.irill.org 

--

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs


Gmane