[Caml-list] FroCoS 2017 - 2nd Call for Papers

[Caml-list] FroCoS 2017 - 2nd Call for Papers

[Geoff Sutcliffe]

           *** Apologies for multiple copies, please redistribute ***

                         SECOND CALL FOR PAPERS

                             FroCoS 2017
   11th International Symposium on Frontiers of Combining Systems
                            Brasilia, Brazil
                         September 25-29th, 2017
                       http://frocos2017.cic.unb.br


Submission Deadlines: 24th April 2017 (abstracts)
                       28th April 2017 (full papers)


GENERAL INFORMATION
   The 11th International Symposium on Frontiers of Combining Systems
   (FroCoS 2017) will be held in Brasilia, Brazil, between September 25 to
   September 29, 2017. Its main goal is to disseminate and promote
   progress in research areas related to the development of techniques
   for the integration, combination, and modularization of formal
   systems together with their analysis.

   FroCoS 2017 will be co-located with the 26th International
   Conference on Automated Reasoning with Analytic Tableaux and Related
   Methods (TABLEAUX 2017) and the 8th International Conference on
   Interactive Theorem Proving (ITP 2017). The local organization of
   all events will be organised  by Claudia Nalon (USB, Brazil),
   Daniele Nantes (UnB, Brazil), Elaine Pimentel (UFRN, Brazil) and
   Joao Marcos (UFRN, Brazil).

SCOPE OF CONFERENCE
   In various areas of computer science, such as logic, computation,
   program development and verification, artificial intelligence,
   knowledge representation, and automated reasoning, there is an
   obvious need for using specialized formalisms and inference systems
   for selected tasks. To be usable in practice, these specialized
   systems must be combined with each other and integrated into general
   purpose systems. This has led---in many research areas---to the
   development of techniques and methods for the combination and
   integration of dedicated formal systems, as well as for their
   modularization and analysis.

   The International Symposium on Frontiers of Combining Systems
   (FroCoS) traditionally focusses on these types of research questions
   and activities. Like its predecessors, FroCoS 2017 seeks to offer a
   common forum for research in the general area of combination,
   modularization, and integration of systems, with emphasis on
   logic-based ones, and of their practical use.

   Typical topics of interest include (but are not limited to):
     * combinations of logics (such as higher-order, first-order,
       temporal, modal, description or other non-classical logics);
     * combination and integration methods in SAT and SMT solving;
     * combination of decision procedures, satisfiability
       procedures, constraint solving techniques, or logical
       frameworks;
     * combinations and modularity in ontologies;
     * integration of equational and other theories into deductive
       systems;
     * hybrid methods for deduction, resolution and constraint
       propagation;
     * hybrid systems in knowledge representation and natural
       language semantics;
     * combined logics for distributed and multi-agent systems;
     * logical aspects of combining and modularizing programs and
       specifications;
     * integration of data structures into constraint logic
       programming and deduction;
     * combinations and modularity in term rewriting;
     * applications of methods and techniques to the verification and
       analysis of information systems.

INVITED SPEAKERS
     - Katalin Bimbo (University of Alberta, Canada) (joint with TABLEAUX 
and ITP)
     - Jasmin Blanchette (Inria and LORIA, Nancy, France) (joint with 
TABLEAUX and ITP)
     - Cezary Kaliszyk (University of Innsbruck, Austria) (joint with 
TABLEAUX and ITP)
     - Cesare Tinelli (University of Iowa, USA)
     - Renata Wassermann (University of Sao Paulo, Brazil)

PUBLICATION DETAILS
   The proceedings of the symposium will be published in the
   Springer LNAI/LNCS series.

PAPER SUBMISSIONS
   The program committee seeks high-quality submissions describing
   original work, written in English, not overlapping with published or
   simultaneously submitted work to a journal or conference with
   archival proceedings. Selection criteria include accuracy and
   originality of ideas, clarity and significance of results, and
   quality of presentation. The page limit in Springer LNCS style is 16
   pages.

   Papers must be edited in LaTeX using the llncs style and must be
   submitted electronically as PDF files via the EasyChair system at
   the following address:

         https://easychair.org/conferences/?conf=frocos2017

   For each accepted paper, at least one of the authors is required to
   attend the symposium and present the work. Prospective authors must
   register a title and an abstract five days before the paper
   submission deadline. Further information about paper submissions is
   available at the conference website that can be found at the
   beginning of this call for papers.

WORKSHOPS AND TUTORIALS
   Proposals for Workshops and Tutorial sessions have been solicited
   in a separate call, which can be found at
   http://frocos2017.cic.unb.br/#cfw.

IMPORTANT DATES
   24th April 2017: Abstract submission deadline
   28th April 2017: Full paper submission deadline
    9th June  2017: Author notification
   23rd June  2017: Camera-ready version due
   September 25-29, 2017: FroCoS Conference

PROGRAM COMMITTEE
  Carlos Areces, FaMAF - Universidad Nacional de Cordoba
  Alessandro Artale, Free University of Bolzano-Bozen
  Mauricio Ayala-Rincon, Universidade de Brasilia
  Franz Baader, TU Dresden
  Peter Baumgartner, National ICT Australia
  Christoph Benzmueller, Freie Universitaet Berlin
  Thomas	Bolander, Technical University of Denmark
  Marcelo Coniglio, State University of Campinas
  Clare Dixon, University of Liverpool [co-chair]
  Francois Fages, Inria Paris-Rocquencourt
  Marcelo Finger, Universidade de Sao Paulo [co-chair]
  Pascal Fontaine, LORIA, INRIA, University of Lorraine
  Didier Galmiche, LORIA, University of Lorraine
  Vijay Ganesh, University of Waterloo
  Silvio Ghilardi, Universita degli Studi di Milano
  Juergen Giesl, RWTH Aachen
  Laura Giordano, Universita del Piemonte Orientale
  Agi Kurucz, Kings College, London
  Till Mossakowski, Otto-von-Guericke-University Magdeburg
  Claudia Nalon, University of Brasilia
  Elaine Pimentel, Universidade Federal do Rio Grande do Norte
  Silvio Ranise, Fondazione Bruno Kessler-Irst
  Christophe Ringeissen, LORIA-INRIA
  Uli Sattler, University of Manchester
  Roberto Sebastiani, University of Trento
  Guillermo Simari, Universidad Nacional del Sur in Bahia Blanca
  Viorica Sofronie-Stokkermans, University Koblenz-Landau
  Andrzej Szalas, University of Warsaw
  Rene Thiemann, University of Innsbruck
  Ashish Tiwari, SRI International
  Christoph Weidenbach, Max Planck Institute for Informatics

[Caml-list] where are we on the Hoogle for OCaml front?

[Francois BERENGER]

Hello,

Do we have a hoogle[1] equivalent that is in production for OCaml?

I mean something that would index all source code available in opam
and allow queries by type signature or keyword?

Currently, I use ocp-browser but I still feel like
it's a temporary and not super efficient measure.

I don't know how to do query by type signature with it.
And many packages don't install their doc so you cannot
see the doc for each function.
At list for the stdlib it works (inside ocp-browser you type List.map 
then spacebar, for example).

When I was an Haskell programmer (for two months, a long time ago), I 
felt Hoogle was the biggest productivity enhancer (you don't reinvent
the wheel, just find which one you need and use it).

Regards,
F.

[1] https://www.haskell.org/hoogle/

Re: [Caml-list] where are we on the Hoogle for OCaml front?

[Jacques Garrigue]

For search by type signature you can use Jun Furuse's OCamlOScope:

https://camlspotter.github.io/ocamloscope.html

It also gives documentation when available.

I'm not sure how big the database is.

Jacques

On 2017/01/28 01:39, Francois BERENGER wrote:
> 
> Hello,
> 
> Do we have a hoogle[1] equivalent that is in production for OCaml?
> 
> I mean something that would index all source code available in opam
> and allow queries by type signature or keyword?
> 
> Currently, I use ocp-browser but I still feel like
> it's a temporary and not super efficient measure.
> 
> I don't know how to do query by type signature with it.
> And many packages don't install their doc so you cannot
> see the doc for each function.
> At list for the stdlib it works (inside ocp-browser you type List.map then spacebar, for example).
> 
> When I was an Haskell programmer (for two months, a long time ago), I felt Hoogle was the biggest productivity enhancer (you don't reinvent
> the wheel, just find which one you need and use it).
> 
> Regards,
> F.
> 
> [1] https://www.haskell.org/hoogle/

Re: [Caml-list] where are we on the Hoogle for OCaml front?

[Hendrik Boom]

On Mon, Feb 06, 2017 at 04:46:02PM +0100, Daniel Bünzli wrote:
> On Saturday, 4 February 2017 at 04:58, Jacques Garrigue wrote:
> > For search by type signature you can use Jun Furuse's OCamlOScope:
> 
> I'm a little bit curious. While I can see the benefit of having general full text search over value identifiers, type identifier and doc strings I was always a little bit dubious about type signature search -- in the end ML types for themselves are a rather weak specification language (I'm not talking about the invariants you may hide behind those of course).
> 
> So beyond curiosity searches are actually people seriously using this to lookup a value they might need ? 

Search on parts of the type, even.  It is very useful to find all the 
functions that do anything with values of a particular type in order 
to find out what you can do with it.  As well as how you can produce 
values of that type.

-- hendrik

Re: [Caml-list] where are we on the Hoogle for OCaml front?

[Francois BERENGER]

On 02/03/2017 09:58 PM, Jacques Garrigue wrote:
> For search by type signature you can use Jun Furuse's OCamlOScope:
>
> https://camlspotter.github.io/ocamloscope.html
>
> It also gives documentation when available.
>
> I'm not sure how big the database is.

It would be nice if the database was containing everything that is in opam.
Or, at least the latest version of anything that is in opam.

Is it really "production ready"?

Should we all jump on it?

Will it stay online for some years?

> Jacques
>
> On 2017/01/28 01:39, Francois BERENGER wrote:
>>
>> Hello,
>>
>> Do we have a hoogle[1] equivalent that is in production for OCaml?
>>
>> I mean something that would index all source code available in opam
>> and allow queries by type signature or keyword?
>>
>> Currently, I use ocp-browser but I still feel like
>> it's a temporary and not super efficient measure.
>>
>> I don't know how to do query by type signature with it.
>> And many packages don't install their doc so you cannot
>> see the doc for each function.
>> At list for the stdlib it works (inside ocp-browser you type List.map then spacebar, for example).
>>
>> When I was an Haskell programmer (for two months, a long time ago), I felt Hoogle was the biggest productivity enhancer (you don't reinvent
>> the wheel, just find which one you need and use it).
>>
>> Regards,
>> F.
>>
>> [1] https://www.haskell.org/hoogle/
>
>
>

Re: [Caml-list] where are we on the Hoogle for OCaml front?

[Daniel Bünzli]

On Saturday, 4 February 2017 at 04:58, Jacques Garrigue wrote:
> For search by type signature you can use Jun Furuse's OCamlOScope:

I'm a little bit curious. While I can see the benefit of having general full text search over value identifiers, type identifier and doc strings I was always a little bit dubious about type signature search -- in the end ML types for themselves are a rather weak specification language (I'm not talking about the invariants you may hide behind those of course).

So beyond curiosity searches are actually people seriously using this to lookup a value they might need ? 

Best, 

Daniel

Re: [Caml-list] where are we on the Hoogle for OCaml front?

[Daniel Bünzli]

On Monday, 6 February 2017 at 15:02, Hendrik Boom wrote:
> It is very useful to find all the 
> functions that do anything with values of a particular type in order 
> to find out what you can do with it. As well as how you can produce 
> values of that type.

Sure but boolean queries on type identifiers seems enough for this. Of course you can always wish to be more precise --- I want this type to appear in that position --- but I'm not sure that's an information need users often have.


D  

Re: [Caml-list] where are we on the Hoogle for OCaml front?

[Ivan Gotovchits]

[-- Attachment #1: Type: text/plain, Size: 1043 bytes --]

On Mon, Feb 6, 2017 at 9:02 AM, Hendrik Boom <hendrik@topoi.pooq.com> wrote:

>
> Search on parts of the type, even.  It is very useful to find all the
> functions that do anything with values of a particular type in order
> to find out what you can do with it.  As well as how you can produce
> values of that type.
>
> Yep, the same as it is done in Coq's search command, where you query all
functions that produce integer

       Search (_ -> int)

It is extremely useful in Coq, and should be as well in OCaml.

For example, when I see, that a function requires a value of type
`Uuidm.t`, then a search for `_ -> Uuidm.t` will reveal all possible ways
to create it.
(Of course, I can just go to the mli file, and read it, but this defeats
the whole purpose of searching).

Regards,
Ivan





> -- hendrik
>
> --
> 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
>

[-- Attachment #2: Type: text/html, Size: 2167 bytes --]

Re: [Caml-list] where are we on the Hoogle for OCaml front?

[Daniel Bünzli]

On Monday, 6 February 2017 at 17:01, Ivan Gotovchits wrote:
> For example, when I see, that a function requires a value of type `Uuidm.t`, then a search for `_ -> Uuidm.t` will reveal all possible ways to create it.

So domain vs range position seems a useful distinction. 

D

Re: [Caml-list] where are we on the Hoogle for OCaml front?

[Ivan Gotovchits]

[-- Attachment #1: Type: text/plain, Size: 1254 bytes --]

On Mon, Feb 6, 2017 at 11:00 AM, Daniel Bünzli <daniel.buenzli@erratique.ch>
wrote:

> On Monday, 6 February 2017 at 15:02, Hendrik Boom wrote:
> > It is very useful to find all the
> > functions that do anything with values of a particular type in order
> > to find out what you can do with it. As well as how you can produce
> > values of that type.
>
> Sure but boolean queries on type identifiers seems enough for this. Of
> course you can always wish to be more precise --- I want this type to
> appear in that position --- but I'm not sure that's an information need
> users often have.



That's why the search should be up-to some isomorphism, e.g.,

     int -> float -> bool


is isomoprhic to

   float -> int -> bool


The seach should also work correctly with lots of aliases, since it is
usual when the same type or value in OCaml has mutliple names. The seach
should also ignore parameter names,
as this is not what a user can know in advance.



>
>
> D
>
>
>
> --
> 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
>

[-- Attachment #2: Type: text/html, Size: 2333 bytes --]

Re: [Caml-list] where are we on the Hoogle for OCaml front?

[Ivan Gotovchits]

[-- Attachment #1: Type: text/plain, Size: 1571 bytes --]

This is a link [1] to the underlying theory of type isomorphism search, for
those who are interested:

[1]: http://www.dicosmo.org/ResearchThemes/ISOS/ISOShomepage.html

On Mon, Feb 6, 2017 at 11:07 AM, Ivan Gotovchits <ivg@ieee.org> wrote:

>
>
> On Mon, Feb 6, 2017 at 11:00 AM, Daniel Bünzli <
> daniel.buenzli@erratique.ch> wrote:
>
>> On Monday, 6 February 2017 at 15:02, Hendrik Boom wrote:
>> > It is very useful to find all the
>> > functions that do anything with values of a particular type in order
>> > to find out what you can do with it. As well as how you can produce
>> > values of that type.
>>
>> Sure but boolean queries on type identifiers seems enough for this. Of
>> course you can always wish to be more precise --- I want this type to
>> appear in that position --- but I'm not sure that's an information need
>> users often have.
>
>
>
> That's why the search should be up-to some isomorphism, e.g.,
>
>      int -> float -> bool
>
>
> is isomoprhic to
>
>    float -> int -> bool
>
>
> The seach should also work correctly with lots of aliases, since it is
> usual when the same type or value in OCaml has mutliple names. The seach
> should also ignore parameter names,
> as this is not what a user can know in advance.
>
>
>
>>
>>
>> D
>>
>>
>>
>> --
>> 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
>>
>
>

[-- Attachment #2: Type: text/html, Size: 3063 bytes --]

Re: [Caml-list] where are we on the Hoogle for OCaml front?

[Daniel Bünzli]

On Monday, 6 February 2017 at 17:07, Ivan Gotovchits wrote:
> That's why the search should be up-to some isomorphism, e.g.,
> 
> int -> float -> bool
> 
> 
> is isomoprhic to
> 
> float -> int -> bool

The papers you mention seem to be about the type ismorophism theory but I can't see any that tries to asses end-user information needs and retrieval evaluation. I'm not sure you need the full theory to build an effective system to support a programmer, e.g. what about the effectiveness of a full type isomorphism search vs a bag of type identifiers with functional position model. Meaningfully limiting the query power to an IR system is a problem in practice, for space, computational and user interface reasons.

D

Re: [Caml-list] where are we on the Hoogle for OCaml front?

[Ivan Gotovchits]

[-- Attachment #1: Type: text/plain, Size: 1811 bytes --]

Well yes, the theory is not required, but it is better to know one :) I
provided a link mostly because it is a sort of a homepage for
type-isomorphic search. There are links to the CamlLight implementations
(yeah the idea was there for some time) and Haskel. Speaking of modern
implementations, Argot [1] is the only example that comes to mind. It has
the isomorphic search and a type manifest search. The search is implemented
mostly in Javascript (generated from OCaml). (Probably, you heard the story
that it is broken and abandoned, and yadda yadda...)

The digest of the theory, is that we have the following rules:

1. a -> b -> c ~ b -> a -> c
2. a * b -> c ~ a -> b -> c
3. unit -> a ~ a

And by applying these rules recursively we can build a set of types that
are isomorphic to the query (or partition all the types into the
isomoprhism groups).


[1]: http://ocaml.github.io/platform-dev/packages/argot/



On Mon, Feb 6, 2017 at 11:34 AM, Daniel Bünzli <daniel.buenzli@erratique.ch>
wrote:

> On Monday, 6 February 2017 at 17:07, Ivan Gotovchits wrote:
> > That's why the search should be up-to some isomorphism, e.g.,
> >
> > int -> float -> bool
> >
> >
> > is isomoprhic to
> >
> > float -> int -> bool
>
> The papers you mention seem to be about the type ismorophism theory but I
> can't see any that tries to asses end-user information needs and retrieval
> evaluation. I'm not sure you need the full theory to build an effective
> system to support a programmer, e.g. what about the effectiveness of a full
> type isomorphism search vs a bag of type identifiers with functional
> position model. Meaningfully limiting the query power to an IR system is a
> problem in practice, for space, computational and user interface reasons.
>
> D
>
>
>

[-- Attachment #2: Type: text/html, Size: 2494 bytes --]

Re: [Caml-list] where are we on the Hoogle for OCaml front?

[Frédéric Bour]

[-- Attachment #1: Type: text/plain, Size: 2453 bytes --]

The experimental version of Merlin implements a similar feature (however 
it looks only in loaded packages, not the whole opam universe).

It is based on names (normalizing type constructors to resolve aliases), 
and uses variance information (types occurring in positive and negative 
positions) to guide the search.

The prototype query language looks like "-int +string" for "string of 
int". You can see a demo here: 
http://alfred.lakaban.net/~def/polarity.webm .


On 06/02/2017 16:46, Ivan Gotovchits wrote:
> Well yes, the theory is not required, but it is better to know one :) 
> I provided a link mostly because it is a sort of a homepage for 
> type-isomorphic search. There are links to the CamlLight 
> implementations (yeah the idea was there for some time) and Haskel. 
> Speaking of modern implementations, Argot [1] is the only example that 
> comes to mind. It has the isomorphic search and a type manifest 
> search. The search is implemented mostly in Javascript (generated from 
> OCaml). (Probably, you heard the story that it is broken and 
> abandoned, and yadda yadda...)
>
> The digest of the theory, is that we have the following rules:
>
> 1. a -> b -> c ~ b -> a -> c
> 2. a * b -> c ~ a -> b -> c
> 3. unit -> a ~ a
>
> And by applying these rules recursively we can build a set of types 
> that are isomorphic to the query (or partition all the types into the 
> isomoprhism groups).
>
>
> [1]: http://ocaml.github.io/platform-dev/packages/argot/
>
>
>
> On Mon, Feb 6, 2017 at 11:34 AM, Daniel Bünzli 
> <daniel.buenzli@erratique.ch <mailto:daniel.buenzli@erratique.ch>> wrote:
>
>     On Monday, 6 February 2017 at 17:07, Ivan Gotovchits wrote:
>     > That's why the search should be up-to some isomorphism, e.g.,
>     >
>     > int -> float -> bool
>     >
>     >
>     > is isomoprhic to
>     >
>     > float -> int -> bool
>
>     The papers you mention seem to be about the type ismorophism
>     theory but I can't see any that tries to asses end-user
>     information needs and retrieval evaluation. I'm not sure you need
>     the full theory to build an effective system to support a
>     programmer, e.g. what about the effectiveness of a full type
>     isomorphism search vs a bag of type identifiers with functional
>     position model. Meaningfully limiting the query power to an IR
>     system is a problem in practice, for space, computational and user
>     interface reasons.
>
>     D
>
>
>


[-- Attachment #2: Type: text/html, Size: 4359 bytes --]

Re: [Caml-list] where are we on the Hoogle for OCaml front?

[Francois BERENGER]

On 02/06/2017 09:46 AM, Daniel Bünzli wrote:
> On Saturday, 4 February 2017 at 04:58, Jacques Garrigue wrote:
>> For search by type signature you can use Jun Furuse's OCamlOScope:
>
> I'm a little bit curious. While I can see the benefit of having general full text search over value identifiers, type identifier and doc strings I was always a little bit dubious about type signature search -- in the end ML types for themselves are a rather weak specification language (I'm not talking about the invariants you may hide behind those of course).

For sure, a plain text search is also very useful and should be provided 
by such a tool (a search "a la Google"; by keywords).

> So beyond curiosity searches are actually people seriously using this to lookup a value they might need ?

But, when you have no idea of how people call the function you are 
looking for, you would go for the search by type signature.

And, because you are not lucky every time, the "hoogle for ocaml" should 
also give you interesting results even when the type signature you have 
input contains some errors.
Like, if the type signature you typed does not exist, you may be 
interested by the closest matching type signature.