2017-04-28

[Caml-list] Formal Methods in Computer-Aided Design - Final Call for Papers

FINAL CALL FOR PAPERS - DEADLINE EXTENSION

International Conference on
Formal Methods in Computer-Aided Design (FMCAD)
Vienna, Austria, October 2-6, 2017

http://www.fmcad.org/FMCAD17


IMPORTANT DATES

Abstract Submission: May 08, 2017
Paper Submission: May 15, 2017
Author Response Period: June 19-23, 2017
Author Notification: July 14, 2017
Camera-Ready Version: Aug 09, 2017

All deadlines are 11:59 pm AoE (Anywhere on Earth)

FMCAD Tutorial Day: October 2, 2017
FMCAD Regular Program: October 3-6, 2017

Part of the FMCAD 2017 program:
- Symposium in memoriam of Helmut Veith
- Hardware Model Checking Competition 2017
- FMCAD Student Forum (deadline: July 21, 2017)

Limited funds will be available for travel assistance for
students with accepted contributions at the student forum.

Co-located event: MEMOCODE 2017 (http://memocode.irisa.fr/2017/)


CONFERENCE SCOPE AND PUBLICATION

FMCAD 2017 is the seventeenth in a series of conferences on the theory and
applications of formal methods in hardware and system verification. FMCAD
provides a leading forum to researchers in academia and industry for
presenting and discussing groundbreaking methods, technologies, theoretical
results, and tools for reasoning formally about computing systems. FMCAD
covers formal aspects of computer-aided system design including verification,
specification, synthesis, and testing.

FMCAD employs a rigorous peer-review process. Accepted papers are distributed
through both ACM and IEEE digital libraries. In addition, published articles
are made available freely on the conference page; 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. A
small number of outstanding FMCAD submissions will be considered for
inclusion in a Special Issue of the journal on Formal Methods in System
Design (FMSD).


TOPICS OF INTEREST

FMCAD welcomes submission of papers reporting original research on advances
in all aspects of formal methods and their applications to computer-
aided design. Topics of interest include (but are not limited to):

-- 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 systems, cyber-physical systems, automotive systems and
other safety-critical systems, hardware-software co-design and
verification, and 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 methods.

-- Application of formal methods to verifying safety, correctness,
connectivity, and security properties of networks and distributed
systems.


SUBMISSIONS

Submissions must be made electronically in PDF format via EasyChair:

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

Two categories of papers are invited: Regular papers, and Tool & Case Study
papers. Regular papers are expected to offer novel foundational ideas,
theoretical results, or algorithmic improvements to existing methods,
along with experimental impact validation where applicable. Tool & Case
Study papers are expected to report on the design, implementation or use of
verification (or related) technology in a practically relevant context
(which need not be industrial), and its impact on design processes.

Both Regular and Tool & Case study papers must use the IEEE Transactions
format on letter-size paper with a 10-point font size. Regular papers can be
up to 8 pages in length and tool papers up to 4 pages, although there
is no requirement to fill all pages in either category. Authors will be
required to select the appropriate paper category at abstract submission
time. Submissions may contain an optional appendix, which will not appear
in the final version of the paper. The reviewers should be able to assess
the quality and the relevance of the results in the paper without reading
the appendix.

Submissions in both categories must contain original research that has not
been previously published, nor is 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 the reviewers access to their data at
submission time, so that results can be independently verified.

FMCAD 2017 COMMITTEES

PROGRAM CHAIRS:

Daryl Stewart, ARM
Georg Weissenbacher, TU Wien

STUDENT FORUM CHAIR:

Keijo Heljanko, Aalto University

LOCAL ARRANGEMENTS CHAIR & WEBMASTER:

Jens Katelaan, TU Wien

PUBLICATION CHAIR:

Mitra Tabaei Befrouei, TU Wien

PROGRAM COMMITTEE

Jade Alglave University College London and Microsoft Research
Christel Baier Technical University of Dresden
Roderick Bloem Graz University of Technology
Hana Chockler King's College London
Andreas Griesmayer ARM
Arie Gurfinkel University of Waterloo
Ziyad Hanna Cadence Design Systems
Fei He Tsinghua University
Alan J. Hu University of British Columbia
Warren A. Hunt Jr. University of Texas
Alexander Ivrii IBM
Barbara Jobstmann EPFL and Cadence Design Systems
Dejan Jovanovic SRI International
Gerwin Klein Data61 and UNSW Australia
Igor Konnov TU Wien
Rebekah Leslie-Hurd Intel
Ines Lynce INESC-ID/IST, Universidade de Lisboa
Ken McMillan Microsoft Research
Charles Morisset Newcastle University
Lee Pike Galois Inc.
Mitra Purandare IBM
Ajitha Rajan University of Edinburgh
Ahmed Rezine Linköping University
Sean Safarpour Synopsys
Roopsha Samanta Purdue University
Martina Seidl Johannes Kepler University Linz
Natasha Sharygina USI Lugano
Anna Slobodova Centaur Technology
Ana Sokolova University of Salzburg
Daryl Stewart ARM
Murali Talupur FormalSim
Michael Tautschnig Queen Mary University of London
Thomas Wahl Northeastern University
Chao Wang University of Southern California
Georg Weissenbacher TU Wien
Florian Zuleger TU Wien

FMCAD STEERING COMMITTEE

Armin Biere, Johannes Kepler University in Linz, Austria
Alan Hu, University of British Columbia, Canada
Warren A. Hunt Jr., University of Texas at Austin, USA
Vigyan Singhal, Oski Tech

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

[Caml-list] Trends in Functional Programming in Education TFPIE 2017, Canterbury 22 June, SECOND CALL FOR PAPERS

TFPIE 2017

Trends in Functional Programming in Education, 2017

https://www.cs.kent.ac.uk/people/staff/sjt/TFPIE2017/


The sixth workshop on Trends in Functional Programming in Education, 2017, which is to be held on the Canterbury campus of the University of Kent on Thursday, 22 June, following the 2017 TFP meeting on 19–21 June. TFPIE workshops have previously been held in St Andrews, Scotland (2012), Provo Utah, USA (2013), Soesterberg, The Netherlands (2014), and Sophia-Antipolis, France (2015), College Park, USA (2016).

A particular topic of this year's TFPIE will be MOOCs and other online learning, and as well as a session on this, we're looking forward to announcing a keynote speaker in this area very soon.

The goal of TFPIE is to gather researchers, teachers and professionals that use, or are interested in the use of, functional programming in education. TFPIE aims to be a venue where novel ideas, classroom-tested ideas and work-in-progress on the use of functional programming in education are discussed. The one-day workshop will foster a spirit of open discussion by having a review process for publication after the workshop. The program chair of TFPIE 2017 will screen submissions to ensure that all presentations are within scope and are of interest to participants. After the workshop, presenters will be invited to submit revised versions of their articles for publication in the journal Electronic Proceedings in Theoretical Computer Science (EPTCS).

Second call for papers

TFPIE 2017 welcomes submissions describing techniques used in the classroom, tools used in and/or developed for the classroom and any creative use of functional programming (FP) to aid education in or outside Computer Science. Topics of interest include, but are not limited to:

- FP and beginning CS students
- FP and Computational Thinking
- FP and Artificial Intelligence
- FP in Robotics
- FP and Music
- Advanced FP for undergraduates
- FP in graduate education
- Engaging students in research using FP
- FP in Programming Languages
- FP in the high school curriculum
- FP as a stepping stone to other CS topics
- FP and Philosophy
- The pedagogy of teaching FP
- FP and e-learning: MOOCs, automated assessment etc.
- Best Lectures – more details below

In addition to papers, we are requesting best lecture presentations. What's your best lecture topic in an FP related course? Do you have a fun way to present FP concepts to novices or perhaps an especially interesting presentation of a difficult topic? In either case, please consider sharing it. Best lecture topics will be selected for presentation based on a short abstract describing the lecture and its interest to TFPIE attendees.

Submission

Potential presenters are invited to submit an extended abstract (4-6 pages) or a draft paper (up to 16 pages) in EPTCS style. The authors of accepted presentations will have their preprints and their slides made available on the workshop's website.

Papers and abstracts can be submitted via easychair at the following link: https://easychair.org/conferences/?conf=tfpie2017

After the workshop, presenters will be invited to submit (a revised version of) their article for review. The PC will select the best articles for publication in the journal Electronic Proceedings in Theoretical Computer Science (EPTCS). Articles rejected for presentation and extended abstracts will not be formally reviewed by the PC.

Programme committee

Dr Laura Castro, University of A Coruña
Prof Ralf Lämmel, University of Koblenz-Landau
Dr Elena Machkasova, University of Minnesota, Morris
Prof Michel Mauny, Inria, Paris
Dr Jeremy Singer, University of Glasgow
Prof Simon Thompson, University of Kent (chair)

Important dates

Submissions of draft papers: 10 May, 2017
Notification: 17 May, 2017
Registration: 11 June, 2017
Workshop: 22 June 2017
Submission for formal review: 18 August, 2017
Notification of acceptance: 6 October, 2017
Camera ready paper: 3 November, 2017



Simon Thompson | Professor of Logic and Computation
School of Computing | University of Kent | Canterbury, CT2 7NF, UK
s.j.thompson@kent.ac.uk | M +44 7986 085754 | W www.cs.kent.ac.uk/~sjt


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

2017-04-26

[Caml-list] 4th Vampire Workshop - Call for Papers

=========================
Vampire 2017: The 4th Vampire Workshop
August 7, 2017, part of CADE 2017
Gothenburg, Sweden

http://easychair.org/smart-program/Vampire17/index.html

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


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

IMPORTANT DATES:

Submission deadline: July 1, 2017
Notification of acceptance: July 7, 2017
Workshop day: August 7, 2017

WORKSHOP AIM:
The workshop aims at discussing the development and use of the first-order
theorem prover Vampire. The workshop will address the newest trends in
implementing first-order theorem provers, and focus on new challenges and
application areas.

Workshop participants will include both Vampire developers and users and
provides a convenient opportunity for interesting discussions between tool
developers and users. The users can learn more about Vampire and its recent
developments. The developers can learn more about the use of Vampire, its
efficiency in various application areas and needs of the users.

The workshop is going to to shed the light on on problems such as

- what is essential for substantial progress in theorem proving tools;
- what are the best implementation principles to be used;
- what are the best heuristics and strategies, depending on application
areas;
- both successful and unsuccessful case studies;
- missing features in modern theorem provers.

The workshop will also overview the most recent advances made in Vampire.

PAPER SUBMISSION:
We seek submissions reporting on theory, application, case studies,
experiments and work-in-progress using Vampire and other theorem provers
in various applications. Submissions can be in any form, ranging from work
in progress to completed work. For example, the users can submit:
- extended abstracts or full papers;
- theoretical papers;
- experimental papers and case studies
- or in general any papers that can benefit tool developers and users.

Papers can be of any length, ranging from 2-page abstracts to full papers
up to 20 pages in length. The papers should use the EasyChair LaTeX,
Microsoft Word, or ODT templates, which can be found at:

http://www.easychair.org/publications/epic-templates.

Submissions should be made using EasyChair, via the link :
https://easychair.org/conferences/?conf=vampire17

The workshop proceedings will be published in the EasyChair EPiC series.


PROGRAM CHAIRS:
Laura Kovacs (Vienna University of Technology)
Andrei Voronkov (University of Manchester, Chalmers University of
Technology and EasyChair)

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

2017-04-25

[Caml-list] ARCADE - 2nd Call for Papers

****************************************************************

*** CALL FOR PAPERS ***

ARCADE http://www.cs.man.ac.uk/~regerg/arcade/
Automated Reasoning:
Challenges, Applications, Directions, Exemplary achievements

6 August 2017, Gothenburg, Sweden (co-located with CADE-26)

DESCRIPTION:

The main goal of this workshop is to bring together key people
from various subcommunities of automated reasoning---such as
SAT/SMT, resolution, tableaux, theory-specific calculi (e.g. for
description logic, arithmetic, set theory), interactive theorem
proving---to discuss the present, past, and future of the field.
The intention is to provide an opportunity to discuss broad
issues facing the community.

The structure of the workshop will be informal. We invite
extended abstracts (2-4 pages, using the EasyChair class style
http://www.easychair.org/publications/for_authors) in the form
of non-technical position statements aimed at prompting lively
discussion. The title of the workshop is indicative of the kind
of discussions we would like to encourage:

Challenges: What are the next grand challenges for research on
automated reasoning? Thereby, we refer to problems, solving
which would imply a significant impact (e.g., shift of focus) on
the CADE community and beyond. Roughly ten years ago SMT was one
such challenge.

Applications: Is automated reasoning applicable in real-world
(industrial) scenarios? Should reports on such applications be
encouraged at a venue like CADE, perhaps by means of a special
case study paper category?

Directions: Based on the grand challenges and requirements from
real-world applications, what are the research directions the
community should promote? What bridges between the different
subcommunities of automated reasoning need to be strengthened?
What new communities should be included (if at all)? For
example, following Reiner Hähnle's question in the AAR
Newsletter, is there a place at CADE for research on usable
automated reasoning (in resemblance to the flourishing topic of
usable security)?

Exemplary achievements: What are the landmark achievements of
automated reasoning whose influence reached far beyond the CADE
community itself? What can we learn from those successes when
shaping our future research?

Contributions will be grouped into similar themes and authors
will be invited to make their case within discussion panels.
Authors will then be invited to extend their abstracts (e.g., by
transcripts of the discussion and a summary of the discussion's
outcomes) for inclusion in an EPiC post-proceedings.

IMPORTANT DATES (Anywhere on Earth):

Submission deadline: 12 May 2017
Notification: 23 June 2017
Workshop: 6 August 2017
Post-proceedings deadline: 29 September 2017

PROGRAM COMMITTEE:

Franz Baader, TU Dresden
Christoph Benzmüller, Freie Universität Berlin
Armin Biere, Johannes Kepler University Linz
Nikolaj Bjørner, Microsoft Research
Jasmin Christian Blanchette, Inria Nancy & Loria
Maria Paola Bonacina, Universite degli Studi di Verona
Pascal Fontaine, Loria, Inria, University of Lorraine
Silvio Ghilardi, Universite degli Studi di Milano
Martin Giese, University of Oslo
Jürgen Giesl, RWTH Aachen
Alberto Griggio, FBK-IRST
Reiner Hähnle, TU Darmstadt
Marijn Heule, The University of Texas at Austin
Laura Kovács, Vienna University of Technology
Aart Middeldorp, University of Innsbruck
Neil Murray, SUNY at Albany
David Plaisted, University of North Carolina at Chapel Hill
Andrei Popescu, Middlesex University London
Giles Reger, University of Manchester (co-chair)
Renate Schmidt, The University of Manchester
Stephan Schulz, DHBW Stuttgart
Geoff Sutcliffe, University of Miami
Cesare Tinelli, The University of Iowa
Dmitriy Traytel, ETH Zürich (co-chair)
Andrei Voronkov, The University of Manchester
Christoph Weidenbach, Max Planck Institute for Informatics

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

2017-04-21

[Caml-list] DL 2017 - Last Call for Papers

-------------------------------------------------------------------------------
LAST CALL FOR PAPERS
30th International Workshop on Description Logics, DL 2017
July 18th to July 21st, 2017 - Montpellier, France
http://dl.kr.org/dl2017/
-------------------------------------------------------------------------------

Important Dates *** NO EXTENSIONS POSSIBLE ***
============
Paper registration deadline:
April 28, 2017
Paper submission deadline:
May 8, 2017
Notification of acceptance:
June 12, 2017
Camera-ready copies:
July 3, 2017
Workshop:
July 18-21, 2017

*** NO DEADLINE EXTENSIONS POSSIBLE ***
Due to the IJCAI notification and the approaching of the DL workshop
extensions will not be granted.

Submissions
==========
* Submissions may be of two types:
(1) Papers accepted at some conference can be submitted as accepted elsewhere
together with a 1-page abstract that also specifies where the paper has
been accepted.
(2) Other submissions consist of 11 pages LNCS plus references. There is no
page limit on the list of references. If the paper should not appear in
the proceedings, an additional 1-page abstract has to be submitted.

* For submissions with an additional 1-page abstract, only the abstract is
published in the proceedings. The abstracts might not be indexed in dblp.
This option is designed for authors who wish to announce results that have
been published elsewhere, or which the authors intend to submit or have
already submitted to a venue with an incompatible prior / concurrent
publication policy.
* All submissions may optionally include a clearly marked appendix (e.g., with
additional proofs or evaluation data). The appendix will be read at the
discretion of the reviewers and not included in the proceedings. The
appendix does not need to be in LNCS format.
* Submission page: https://easychair.org/conferences/?conf=dl2017
* Accepted papers and 1-page abstracts will be made available electronically
in the CEUR Workshop Proceedings series (http://www.CEUR-ws.org/).
* Accepted submissions, be they full papers or 1-page abstracts, will be
selected for either oral or poster presentation at the workshop. Submissions
will be judged solely based upon their content, and the type of submission
will have no bearing on the decision between oral and poster presentation.

Further Details
============
http://dl.kr.org/dl2017/


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

2017-04-18

[Caml-list] VSTTE 2017 - Second Call for Papers

9th Working Conference on Verified Software:
Theories, Tools, and Experiments (VSTTE)

https://vstte17.lri.fr

July 22-23, 2017, Heidelberg, Germany

Co-located with the 29th International Conference
on Computer-Aided Verification, CAV 2017


Important Dates

* Abstract submission: Mon, Apr 24, 2017
* Full paper submission: Mon, May 1, 2017
* Notification: Mon, Jun 5, 2017
* VSTTE: Sat-Sun, Jul 22-23, 2017
* Camera-ready: Mon, Aug 21, 2017

Overview

The goal of the VSTTE conference series is to advance the state of the
art in the science and technology of software verification, through the
interaction of theory development, tool evolution, and experimental
validation.

We welcome submissions describing significant advances in the production
of verified software, i.e., software that has been proved to meet its
functional specifications. Submissions of theoretical, practical, and
experimental contributions are equally encouraged, including those
that focus on specific problems or problem domains. We are especially
interested in submissions describing large-scale verification efforts
that involve collaboration, theory unification, tool integration, and
formalized domain knowledge. We also welcome papers describing novel
experiments and case studies evaluating verification techniques and
technologies.

Topics of interest for VSTTE include education, requirements modeling,
specification languages, specification/verification/certification case
studies, formal calculi, software design methods, automatic code generation,
refinement methodologies, compositional analysis, verification tools
(e.g., static analysis, dynamic analysis, model checking, theorem proving,
satisfiability), tool integration, benchmarks, challenge problems, and
integrated verification environments.

Paper Submissions

We accept both long (limited to 16 pages) and short (limited to 10 pages)
paper submissions. Short submissions also cover Verification Pearls
describing an elegant proof or proof technique. Submitted research papers
and system descriptions must be original and not submitted for publication
elsewhere. Each submission will be evaluated by at least three members of
the Program Committee. We expect that one author of every accepted paper
will present their work at the conference.

Paper submissions must be written in English using the LNCS LaTeX format
(http://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines)
and must include a cogent and self-contained description of the ideas,
methods, results, and comparison to existing work.

Papers will be submitted via EasyChair at the VSTTE 2017 conference page
(https://www.easychair.org/conferences/?conf=vstte2017). The post-conference
proceedings of VSTTE 2017 will be published in the LNCS series. Authors
of accepted papers will be requested to sign the copyright transfer form.
A selection of best papers will be invited for publication in the Journal
of Automated Reasoning.

Invited Speakers

* Christoph Weidenbach (Max Planck Institute for Informatics, Germany)
* Santiago Zanella-Beguelin (Microsoft Research, UK)

Program Committee

* June Andronick (University of New South Wales, Australia)
* Christel Baier (TU Dresden, Germany)
* Sandrine Blazy (Université de Rennes 1, France)
* Arthur Charguéraud (Inria, France)
* Ernie Cohen (Amazon Web Services, USA)
* Rayna Dimitrova (MPI-SWS, Germany)
* Carlo A. Furia (Chalmers University of Technology, Sweden)
* Arie Gurfinkel (University of Waterloo, Canada)
* Hossein Hojjat (Rochester Institute of Technology, USA)
* Marieke Huisman (University of Twente, Netherlands)
* Bart Jacobs (KU Leuven, Belgium)
* Rajeev Joshi (NASA Jet Propulsion Laboratory, USA)
* Zachary Kincaid (Princeton University, USA)
* Akash Lal (Microsoft Research, India)
* Shuvendu Lahiri (Microsoft Research, USA)
* Francesco Logozzo (Facebook, USA)
* Peter Müller (ETH Zürich, Switzerland)
* Jorge A. Navas (SRI International, USA)
* Scott Owens (University of Kent, UK)
* Andrei Paskevich (Université Paris-Sud, France), co-chair
* Gerhard Schellhorn (Universität Augsburg, Germany)
* Peter Schrammel (University of Sussex, UK)
* Natarajan Shankar (SRI International, USA)
* Mihaela Sighireanu (Université Paris-Diderot, France)
* Julien Signoles (CEA LIST, France)
* Michael Tautschnig (Queen Mary University of London, UK)
* Tachio Terauchi (JAIST, Japan)
* Oksana Tkachuk (NASA Ames Research Center, USA)
* Mattias Ulbrich (Karlsruhe Institute of Technology, Germany)
* Thomas Wies (New York University, USA), co-chair

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

[Caml-list] Frama-C & SPARK Day: Formal Analysis and Proof for Programs in C and Ada, 30 May 2017 - Call for participation

Call for Participation

Frama-C & SPARK Day 2017:
Formal Analysis and Proof for Programs in C and Ada

Paris, Tuesday, May 30th, 2017

http://frama-c.com/FCSD17.html


We are pleased to invite you to attend Frama-C & SPARK Day 2017.
This one-day workshop aims at gathering both academic and industrial
users of the environments Frama-C and SPARK, for sharing experiences
and discussing perspectives.

Location: Université Paris-Diderot, Amphithéatre Buffon, 15 rue Hélène
Brion, Paris

The program, registration information and travel instructions are
available from

http://frama-c.com/FCSD17.html

Registration is free of charge but necessary.

The workshop takes place in the context of the event `Open Source Innovation
Spring 2017' (http://www.open-source-innovation-spring.org/) initiated by thematic
group `Logiciel libre' of the cluster Systematic-Paris-Region and
IRILL (`Initiative de Recherche et Innovation sur le Logiciel Libre').
It is co-organized by CEA List (http://www-list.cea.fr/en/), AdaCore (http://www.adacore.com/),
Inria joint lab `ProofInUse' (http://www.spark-2014.org/proofinuse), and
Université Paris-Diderot.


--
Nikolai KOSMATOV, PhD
Software Safety Laboratory, CEA LIST
Mail : CEA Saclay Nano-INNOV
Institut CARNOT CEA LIST
DILS/LSL, PC 174
91191 Gif-sur-Yvette Cedex, France
Phone: +33 (0)1 69 08 71 83
Fax: +33 (0)1 69 08 83 95
Email: nikolai.kosmatov@cea.fr


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

2017-04-17

[Caml-list] Call for participation: PLDI 2017 and co-located events

Call for participation: PLDI 2017 and co-located events

PLDI is the premier forum in the field of programming languages and
programming systems research, covering the areas of design,
implementation, theory, applications, and performance. The co-located
conferences take place in Barcelona, June 18-23, 2017. This year, PLDI
is co-located with ECOOP, LCTES, DEBS, ISMM, Curry On and others. The
conferences will take place at the Universitat Polytècnica de Catalunya
in Barcelona, Spain.
http://conf.researchr.org/home/pldi-2017

Registration is now open, please visit:
https://regmaster4.com/2017conf/BARC17/register.php
to register. The early registration rate ends on May 26th.

The tentative program is available at:
http://pldi17.sigplan.org/program/program-pldi-2017

PLDI will also hold an ACM Student Research Competition:
http://pldi17.sigplan.org/track/pldi-2017-student-research-competition


Co-located events:

+ ECOOP: European Conference on Object-Oriented Programming
+ DEBS: annual conference on Distributed Event-Based Systems
+ Curry On: conference on programming languages and emerging challenges
in industry.
+ ISMM: International Symposium on Memory Management
+ LCTES: Languages, Compilers, and Tools for Embedded Systems

Co-located workshops include:

+ ARRAY: Workshop on Libraries, Languages and Compilers for Array
Programming
+ DSW: Deep Specifications in the Wild
+ FMS: Formal Methods for Security
+ IC: Workshop on Incremental Computing
+ MAPL: Machine Learning and Programming Languages
+ PLMW: Programming Languages Mentoring Workshop
+ SOAP: International Workshop on the State Of the Art in Java Program
Analysis
+ WCIRE: Workshop for Compiler Infrastructure for Research and Education

Additionally, there will be eight co-located tutorials:

+ Bug detection in JavaScript web apps using the SAFE framework
+ Building your own modular static analyzer with Facebook Infer
+ Engineering Static Analyzers with Soufflé
+ Graal: High Performance Compilation for Managed Languages
+ P4: Programming the Network Data Plane
+ Polyhedral Compilation
+ Refinement Types for Program Verification and Synthesis
+ Scala, LMS and Delite for High-Performance DSLs and Program Generators
+ WALA Hack-A-Thon
+ Writing Verified Programs in CakeML

See the web site for a schedule and further details and links. For
further updates, follow PLDI on the social media:

Facebook: https://www.facebook.com/PLDIConf
Twitter: https://twitter.com/PLDI

Albert Cohen, PLDI 2017 General Chair
Tobias Grosser, PLDI 2017 Publicity Chair

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

2017-04-12

[Caml-list] Compose Conference Call for Participation [NYC, May 18-19]

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

Call for Participation

Compose Conference 2017

May 18-19 2017
New York, NY

http://www.composeconference.org/2017

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

The practice and craft of functional programming :: Conference

Compose is a conference for typed functional programmers, focused specifically on Haskell, OCaml, F#, SML, and related technologies.

Typed functional programming has been taken up widely, by industry and hobbyists alike. For many of us it has renewed our belief that code should be beautiful, and that programming can be as enjoyable as it is practical. Compose is about bringing together functional programmers of all levels of skill and experience — from technical leads to novices, and from long-time hackers to students just getting started.

It will feature a keynote by Emily Riehl on aspects of category theory and computation, and two days of great talks.

* Invited Talks
Emily Riehl: TBA

* Local Information (venue): http://www.composeconference.org/2017/

* Accepted Talks and Tutorials

Barry Burd - Teaching Haskell
David Rhodes - Learning F#: Case study with branch and bound
Edmund Cape - Multiplying by 1 - an important form of computation and
how it reveals distinctions between kleislis
Enzo Alda, et al. - Reactive Sheets: an intuitive approach to
functional‑reactive computing
Hezekiah Carty and Chris Donaher - Distrest - REST access to
distributed services
Hongbo Zhang - BuckleScript: Making functional programming accessible
to JavaScript developers
Jennifer Paykin, Kenneth Foner, Antal Spector-Zabusky - `choose` Your
Own Derivative
Joachim Breitner - Lock-step simulation is child's play
Martín Ceresa, Gustavo Grieco - QuickFuzz Testing for Fun and Profit
Michael Chavinda - Android programming in Froid
Nikhil Barthwal - Implementing an Event-Driven Microservices
Architecture in F#: A case study of Jet.com
Nikita Volkov - New Hasql - a simpler, safer and faster Postgres client
Sebastien Mondet - Typed-Tagless Final Bioinformatics
Stephen Compall - Working with Monads in OCaml
Stuart Popejoy - Smart Contracts and Formal Verification with Z3 with Pact
Tikhon Jelvis - The Probability Monad
Yaron Minsky - Data Driven UIs, Incrementally

* Full abstracts: http://www.composeconference.org/2017/program

* Registration: http://composeconference.eventbrite.com

* Follow @composeconf on twitter for news: https://twitter.com/composeconf

* On freenode irc, chat with fellow attendees at #composeconference

* Corporate sponsorships are welcome. Current sponsors list forthcoming.

* Policies (diversity and anti-harassment):
http://www.composeconference.org/conduct

* Email us with any questions at info@composeconference.org

* Please forward this announcement to interested parties and lists.

2017-04-11

[Caml-list] Formal Methods in Computer-Aided Design - Call for Papers

2nd CALL FOR PAPERS

International Conference on
Formal Methods in Computer-Aided Design (FMCAD)
Vienna, Austria, October 2-6, 2017

http://www.fmcad.org/FMCAD17


IMPORTANT DATES

Abstract Submission: May 01, 2017
Paper Submission: May 08, 2017
Author Response Period: June 19-23, 2017
Author Notification: July 14, 2017
Camera-Ready Version: Aug 09, 2017

All deadlines are 11:59 pm AoE (Anywhere on Earth)

FMCAD Tutorial Day: October 2, 2017
FMCAD Regular Program: October 3-6, 2017

Part of the FMCAD 2017 program:
- Symposium in memoriam of Helmut Veith
- Hardware Model Checking Competition 2017
- FMCAD Student Forum (deadline: July 21, 2017)

Limited funds will be available for travel assistance for
students with accepted contributions at the student forum.

Co-located event: MEMOCODE 2017 (http://memocode.irisa.fr/2017/)


CONFERENCE SCOPE AND PUBLICATION

FMCAD 2017 is the seventeenth in a series of conferences on the theory and
applications of formal methods in hardware and system verification. FMCAD
provides a leading forum to researchers in academia and industry for
presenting and discussing groundbreaking methods, technologies, theoretical
results, and tools for reasoning formally about computing systems. FMCAD
covers formal aspects of computer-aided system design including verification,
specification, synthesis, and testing.

FMCAD employs a rigorous peer-review process. Accepted papers are distributed
through both ACM and IEEE digital libraries. In addition, published articles
are made available freely on the conference page; 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. A
small number of outstanding FMCAD submissions will be considered for
inclusion in a Special Issue of the journal on Formal Methods in System
Design (FMSD).


TOPICS OF INTEREST

FMCAD welcomes submission of papers reporting original research on advances
in all aspects of formal methods and their applications to computer-
aided design. Topics of interest include (but are not limited to):

-- 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 systems, cyber-physical systems, automotive systems and
other safety-critical systems, hardware-software co-design and
verification, and 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 methods.

-- Application of formal methods to verifying safety, correctness,
connectivity, and security properties of networks and distributed
systems.


SUBMISSIONS

Submissions must be made electronically in PDF format via EasyChair:

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

Two categories of papers are invited: Regular papers, and Tool & Case Study
papers. Regular papers are expected to offer novel foundational ideas,
theoretical results, or algorithmic improvements to existing methods,
along with experimental impact validation where applicable. Tool & Case
Study papers are expected to report on the design, implementation or use of
verification (or related) technology in a practically relevant context
(which need not be industrial), and its impact on design processes.

Both Regular and Tool & Case study papers must use the IEEE Transactions
format on letter-size paper with a 10-point font size. Regular papers can be
up to 8 pages in length and tool papers up to 4 pages, although there
is no requirement to fill all pages in either category. Authors will be
required to select the appropriate paper category at abstract submission
time. Submissions may contain an optional appendix, which will not appear
in the final version of the paper. The reviewers should be able to assess
the quality and the relevance of the results in the paper without reading
the appendix.

Submissions in both categories must contain original research that has not
been previously published, nor is 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 the reviewers access to their data at
submission time, so that results can be independently verified.

FMCAD 2017 COMMITTEES

PROGRAM CHAIRS:

Daryl Stewart, ARM
Georg Weissenbacher, TU Wien

STUDENT FORUM CHAIR:

Keijo Heljanko, Aalto University

LOCAL ARRANGEMENTS CHAIR & WEBMASTER:

Jens Katelaan, TU Wien

PUBLICATION CHAIR:

Mitra Tabaei Befrouei, TU Wien

PROGRAM COMMITTEE

Jade Alglave University College London and Microsoft Research
Christel Baier Technical University of Dresden
Roderick Bloem Graz University of Technology
Hana Chockler King's College London
Andreas Griesmayer ARM
Arie Gurfinkel University of Waterloo
Ziyad Hanna Cadence Design Systems
Fei He Tsinghua University
Alan J. Hu University of British Columbia
Warren A. Hunt Jr. University of Texas
Alexander Ivrii IBM
Barbara Jobstmann EPFL and Cadence Design Systems
Dejan Jovanovic SRI International
Gerwin Klein Data61 and UNSW Australia
Igor Konnov TU Wien
Rebekah Leslie-Hurd Intel
Ines Lynce INESC-ID/IST, Universidade de Lisboa
Ken McMillan Microsoft Research
Charles Morisset Newcastle University
Lee Pike Galois Inc.
Mitra Purandare IBM
Ajitha Rajan University of Edinburgh
Ahmed Rezine Linköping University
Sean Safarpour Synopsys
Roopsha Samanta Purdue University
Martina Seidl Johannes Kepler University Linz
Natasha Sharygina USI Lugano
Anna Slobodova Centaur Technology
Ana Sokolova University of Salzburg
Daryl Stewart ARM
Murali Talupur FormalSim
Michael Tautschnig Queen Mary University of London
Thomas Wahl Northeastern University
Chao Wang University of Southern California
Georg Weissenbacher TU Wien
Florian Zuleger TU Wien

FMCAD STEERING COMMITTEE

Armin Biere, Johannes Kepler University in Linz, Austria
Alan Hu, University of British Columbia, Canada
Warren A. Hunt Jr., University of Texas at Austin, USA
Vigyan Singhal, Oski Tech

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

2017-04-05

[Caml-list] FSCD 2017 - Last Call for Papers (ABSTRACT DEADLINE THIS WEEK)

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

   CALL FOR PAPERS

  Second International Conference on
     Formal Structures for Computation and Deduction (FSCD'17)

  4 -- 7 September 2017, Oxford, UK
(in-cooperation with the ACM SIGLOG and SIGPLAN and co-located with ICFP 2017)
     http://www.cs.ox.ac.uk/conferences/fscd2017/

FSCD (http://fscdconference.org/) covers all aspects of formal
structures for computation and deduction from theoretical foundations
to applications.  Building on two communities, RTA (Rewriting
Techniques and Applications) and TLCA (Typed Lambda Calculi and
Applications), FSCD embraces their core topics and broadens their
scope to closely related areas in logics, proof theory and new
emerging models of computation such as quantum computing or homotopy
type theory.

IMPORTANT DATES All deadlines are midnight anywhere-on-earth (AoE) and
are firm; late submissions will not be considered.

Abstract Deadline:             7 April 2017
Submission Deadline:       14 April 2017
Rebuttal:                           29--31 May   2017
Notification:                      14 June  2017 
Camera-Ready:                7 July  2017 

Suggested, but not exclusive, list of topics for submission are:

1. Calculi: Lambda calculus * Concurrent calculi * Logics * Rewriting
  systems * Proof theory * Type theory and logical frameworks

2. Methods in Computation and Deduction: Type systems * Induction and
  coinduction * Matching, unification, completion, and orderings *
  Strategies * Tree automata * Model checking * Proof search and
  theorem proving * Constraint solving and decision procedures

3. Semantics: Operational semantics * Abstract machines * Game
  Semantics * Domain theory and categorical models * Quantitative
  models

4. Algorithmic Analysis and Transformations of Formal Systems: Type
  Inference and type checking * Abstract Interpretation * Complexity
  analysis and implicit computational complexity * Checking
  termination, confluence, derivational complexity and related
  properties * Symbolic computation

5. Tools and Applications: Programming and proof environments *
  Verification tools * Libraries for proof assistants and interactive
  theorem provers * Case studies in proof assistants and interactive
  theorem provers * Certification

PUBLICATION The proceedings will be published as an electronic volume
in the Leibniz International Proceedings in Informatics (LIPIcs) of
Schloss Dagstuhl. All LIPIcs proceedings are open access.

SUBMISSION GUIDELINES Submissions can be made in two categories.
Regular research papers are limited to 15 pages and must present
original research which is unpublished and not submitted
elsewhere. System descriptions are limited to 10 pages and must
describe a working system which has not been published or submitted
elsewhere.  Submissions must be formatted using the LIPIcs style files
and submitted via EasyChair.  Complete instructions on submitting a
paper can be found on the conference web site.

SPECIAL ISSUES Full versions of several accepted papers, to be
selected by the program committee, will be invited for submission to a
special issue of Logical Methods in Computer Science.

BEST PAPER AWARD BY JUNIOR RESEARCHERS The program committee will
consider declaring this award to a paper in which all authors are
junior researchers: a junior researcher is a person who is either a
student or whose PhD award date is less than three years from the
first day of the meeting.

PROGRAM COMMITTEE CHAIR
 Dale Miller, Inria Saclay & LIX <fscd17@easychair.org>

PROGRAM COMMITTEE
 Andreas Abel, Gothenburg Univ.  
 Elvira Albert, Complutense Madrid 
 Maria Alpuente, TU Valencia 
 Takahito Aoto, Niigata Univ.
 Zena Ariola, Univ. Oregon 
 Federico Aschieri, TU Wien 
 Stefano Berardi, Univ.  Turin 
 Lars Birkedal, Aarhus Univ.
 Filippo Bonchi, CNRS, ENS Lyon 
 Pierre Clairambault, CNRS, ENS Lyon
 Ugo Dal Lago, Univ. Bologna 
 Herman Geuvers, Radboud Univ. 
 Silvia Ghilezan, Univ.  Novi Sad 
 Juergen Giesl, RWTH Aachen 
 Hugo Herbelin, Inria Paris
 Jan Hoffmann, Carnegie Mellon 
 Deepak Kapur, Univ.  New Mexico 
 Paul Blain Levy, Univ.  Birmingham 
 Paulo Oliva, QMUL, London 
 Vincent van Oostrom, Univ. Innsbruck 
 Daniela Petrisan, LIAFA, Paris 
 Femke van Raamsdonk, VU Univ. Amsterdam 
 Grigore Rosu, Univ. Illinois 
 Albert Rubio, UPC-BarcelonaTech
 Paula Severi, Univ.  Leicester 
 Bas Spitters, Aarhus Univ.  
 Aaron Stump, Univ. Iowa 
 Kazushige Terui, Kyoto Univ.
 Rene Thiemann, Univ.  Innsbruck 
 Sophie Tison, Lille Univ.

CONFERENCE CHAIR
 Sam Staton, Univ. of Oxford

WORKSHOP CHAIR
 Jamie Vicary, Univ. of Oxford

PUBLICITY CHAIR
 Sandra Alves, Univ. of Porto

FSCD STEERING COMMITTEE T. Altenkirch (Univ. Nottingham), S. Alves
(Univ. Porto), G. Dowek, (Inria), S. Escobar (Univ. Politecnica de
Valencia), M. Fernandez (King's College London), H. Herbelin (Inria),
D. Kesner (Univ. Paris), N. Kobayashi (Univ. Tokyo), L. Ong (Chair,
Univ. Oxford), B. Pientka (McGill Univ.), R. Thiemann (Univ. Innsbruck).

[Caml-list] 2nd call for papers: Trends in Functional Programming, 19-21 june 2017, University of Kent, Canterbury

-----------------------------
C A L L F O R P A P E R S
-----------------------------

======== TFP 2017 ===========

18th Symposium on Trends in Functional Programming
19-21 June, 2017
University of Kent, Canterbury
https://www.cs.kent.ac.uk/events/tfp17/index.html

The symposium on Trends in Functional Programming (TFP) is an
international forum for researchers with interests in all aspects of
functional programming, taking a broad view of current and future
trends in the area. It aspires to be a lively environment for
presenting the latest research results, and other contributions (see
below). Authors of draft papers will be invited to submit revised
papers based on the feedback receive at the symposium. A
post-symposium refereeing process will then select a subset of these
articles for formal publication.

TFP 2017 will be the main event of a pair of functional programming
events. TFP 2017 will be accompanied by the International Workshop on
Trends in Functional Programming in Education (TFPIE), which will take
place on 22 June.

The TFP symposium is the heir of the successful series of Scottish
Functional Programming Workshops. Previous TFP symposia were held in
* Edinburgh (Scotland) in 2003;
* Munich (Germany) in 2004;
* Tallinn (Estonia) in 2005;
* Nottingham (UK) in 2006;
* New York (USA) in 2007;
* Nijmegen (The Netherlands) in 2008;
* Komarno (Slovakia) in 2009;
* Oklahoma (USA) in 2010;
* Madrid (Spain) in 2011;
* St. Andrews (UK) in 2012;
* Provo (Utah, USA) in 2013;
* Soesterberg (The Netherlands) in 2014;
* Inria Sophia-Antipolis (France) in 2015;
* and Maryland (USA) in 2016.
For further general information about TFP please see the TFP homepage.
(http://www.tifp.org/).


== SCOPE ==

The symposium recognizes that new trends may arise through various
routes. As part of the Symposium's focus on trends we therefore
identify the following five article categories. High-quality articles
are solicited in any of these categories:

Research Articles: leading-edge, previously unpublished research work
Position Articles: on what new trends should or should not be
Project Articles: descriptions of recently started new projects
Evaluation Articles: what lessons can be drawn from a finished project
Overview Articles: summarizing work with respect to a trendy subject

Articles must be original and not simultaneously submitted for
publication to any other forum. They may consider any aspect of
functional programming: theoretical, implementation-oriented, or
experience-oriented. Applications of functional programming
techniques to other languages are also within the scope of the
symposium.

Topics suitable for the symposium include, but are not limited to:

Functional programming and multicore/manycore computing
Functional programming in the cloud
High performance functional computing
Extra-functional (behavioural) properties of functional programs
Dependently typed functional programming
Validation and verification of functional programs
Debugging and profiling for functional languages
Functional programming in different application areas:
security, mobility, telecommunications applications, embedded
systems, global computing, grids, etc.
Interoperability with imperative programming languages
Novel memory management techniques
Program analysis and transformation techniques
Empirical performance studies
Abstract/virtual machines and compilers for functional languages
(Embedded) domain specific languages
New implementation strategies
Any new emerging trend in the functional programming area

If you are in doubt on whether your article is within the scope of
TFP, please contact the TFP 2017 program chairs, Scott Owens and Meng Wang.


== BEST PAPER AWARDS ==

To reward excellent contributions, TFP awards a prize for the best paper
accepted for the formal proceedings.

TFP traditionally pays special attention to research students,
acknowledging that students are almost by definition part of new
subject trends. A student paper is one for which the authors state
that the paper is mainly the work of students, the students are listed
as first authors, and a student would present the paper. A prize for
the best student paper is awarded each year.

In both cases, it is the PC of TFP that awards the prize. In case the
best paper happens to be a student paper, that paper will then receive
both prizes.


== PAPER SUBMISSIONS ==

Acceptance of articles for presentation at the symposium is based on a
lightweight peer review process of extended abstracts (4 to 10 pages
in length) or full papers (20 pages). The submission must clearly
indicate which category it belongs to: research, position, project,
evaluation, or overview paper. It should also indicate which authors
are research students, and whether the main author(s) are students. A
draft paper for which ALL authors are students will receive additional
feedback by one of the PC members shortly after the symposium has
taken place.

We use EasyChair for the refereeing process. Papers must be submitted at:

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

Papers must be written in English, and written using the LNCS
style. For more information about formatting please consult the
Springer LNCS web site:

http://www.springer.com/computer/lncs?SGWID=0-164-6-793341-0

== INVITED SPEAKERS ==
Conor McBride University of Strathclyde (UK)
Cătălin Hriţcu INRIA Paris (FR)


== IMPORTANT DATES ==

Submission of draft papers: 5 May, 2017
Notification: 12 May, 2017
Registration: 11 June, 2017
TFP Symposium: 19-21 June, 2017
Student papers feedback: 29 June, 2017
Submission for formal review: 2 August, 2017
Notification of acceptance: 3 November, 2017
Camera ready paper: 2 December, 2017


== PROGRAM COMMITTEE ==

Co-Chairs
Meng Wang University of Kent (UK)
Scott Owens University of Kent (UK)

PC
Jeremy Yallop University of Cambridge (UK)
Nicolas Wu University of Bristol (UK)
Laura Castro University of A Coruña (ES)
Gabriel Scherer Northeastern University (US)
Edwin Brady University of St Andrews (UK)
Janis Voigtländer Radboud University Nijmegen (NL)
Peter Achten Radboud University Nijmegen (NL)
Tom Schrijvers KU Leuven (BE)
Matthew Fluet Rochester Institute of Technology (US)
Mauro Jaskelioff CIFASIS/Universidad Nacional de Rosario (AG)
Patricia Johann Appalachian State University (US)
Bruno Oliveira The University of Hong Kong (HK)
Rita Loogen Philipps-Universität Marburg (GE)
David Van Horn University of Marylan (US)
Soichiro Hidaka Hosei University (JP)
Michał Pałka Chalmers University of Technology (SE)
Sandrine Blazy University of Rennes 1 - IRISA (FR)



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