2019-10-30

[Caml-list] MSFP 2020 - First Call for Papers

Eighth Workshop on
MATHEMATICALLY STRUCTURED FUNCTIONAL PROGRAMMING
Saturday 25th April 2020, Dublin, Ireland
A satellite workshop of ETAPS 2020

https://msfp-workshop.github.io/msfp2020/

** Deadline: 9th January (abstract), 16th January (paper) **

The eighth workshop on Mathematically Structured Functional
Programming is devoted to the derivation of functionality from
structure. It is a celebration of the direct impact of Theoretical
Computer Science on programs as we write them today. Modern
programming languages, and in particular functional languages, support
the direct expression of mathematical structures, equipping
programmers with tools of remarkable power and abstraction. Where
would Haskell be without monads? Functional reactive programming
without temporal logic? Call-by-push-value without adjunctions? The
list goes on. This workshop is a forum for researchers who seek to
reflect mathematical phenomena in data and control.

The first MSFP workshop was held in Kuressaare, Estonia, in July 2006,
affiliated with MPC 2006 and AMAST 2006. The second MSFP workshop was
held in Reykjavik, Iceland as part of ICALP 2008. The third MSFP
workshop was held in Baltimore, USA, as part of ICFP 2010. The fourth
workshop was held in Tallinn, Estonia, as part of ETAPS 2012. The
fifth workshop was held in Grenoble, France, as part of ETAPS
2014. The sixth MSFP Workshop was held in April 2016, in Eindhoven,
Netherlands, as part of ETAPS 2016. The seventh MSFP Workshop was held
in July 2018, in Oxford, UK, as part of FLoC 2018.

Important Dates:
================

Abstract deadline: 9th January (Thursday)
Paper deadline: 16th January (Thursday)
Notification: 27th February (Thursday)
Final version: 26th March (Thursday)
Workshop: 25th April (Saturday)

Invited Speakers:
=================

- Pierre-Marie Pédrot, Inria Rennes-Bretagne-Atlantique, France
- Second invited speaker TBC

Program Committee:
==================

Stephanie Balzer - CMU, USA
Kwanghoon Choi - Chonnam, South Korea
Ralf Hinze - Kaiserslautern, Germany
Marie Kerjean - Inria Nantes, France
Sam Lindley - Edinburgh and Imperial, UK (co-chair)
Max New - Northeastern, USA (co-chair)
Fredrik Nordvall-Forsberg - Strathclyde, UK
Alberto Pardo - Montevideo, Uruguay
Exequiel Rivas Gadda - Inria Paris, France
Claudio Russo - DFINITY, UK
Tarmo Uustalu - Reykjavik, Iceland
Nicolas Wu - Imperial, UK
Maaike Zwart - Oxford, UK

Submission:
===========

Submissions are welcomed on, but by no means restricted to, topics
such as:

structured effectful computation
structured recursion
structured corecursion
structured tree and graph operations
structured syntax with variable binding
structured datatype-genericity
structured search
structured representations of functions
structured quantum computation
structure directed optimizations
structured types
structure derived from programs and data

Please contact the programme chairs Sam Lindley (Sam.Lindley@ed.ac.uk)
and Max New (maxnew@ccs.neu.edu) if you have any questions about the
scope of the workshop.

We accept two categories of submission: full papers of no more than 15
pages that will appear in the proceedings, and extended abstracts of
no more than 2 pages that we will post on the website, but which do
not constitute formal publications and will not appear in the
proceedings. References and appendices are not included in page
limits. Appendices may not be read by reviewers.

Submissions must report previously unpublished work and not be
submitted concurrently to another conference with refereed
proceedings. Accepted papers must be presented at the workshop by one
of the authors. The proceedings will be published under the auspices
of EPTCS with a Creative Commons license.

A short abstract should be submitted a week in advance of the paper
deadline (for both full paper and extended abstract submissions).

We are using EasyChair to manage submissions. To submit a paper, use
this link:

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

--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

2019-10-16

[Caml-list] Artificial Intelligence and Theorem Proving 2020 - Call for Papers

CALL FOR CONTRIBUTIONS

Artificial Intelligence and Theorem Proving
AITP 2020
March 22-27, 2020, Aussois, France

http://aitp-conference.org/2020

Deadline: December 3, 2019
https://easychair.org/conferences/?conf=aitp2020

BACKGROUND
Large-scale semantic processing and strong computer assistance of mathematics
and science is our inevitable future. New combinations of AI and reasoning
methods and tools deployed over large mathematical and scientific corpora will
be instrumental to this task. The AITP conference is the forum for discussing
how to get there as soon as possible, and the force driving the progress
towards that.

TOPICS
- AI, machine learning and big-data methods in theorem proving and mathematics.
- Collaboration between automated and interactive theorem proving, in
particular their AI/ML aspects.
- Common-sense reasoning and reasoning in science.
- Alignment and joint processing of formal, semi-formal, and informal
libraries, Formal Abstracts.
- Methods for large-scale computer understanding of mathematics and science.
- Combinations of linguistic/learning-based and semantic/reasoning methods
- Formal verification of AI and machine learning algorithms, explainable AI .

SESSIONS
There will be several focused sessions on AI for ATP, ITP and mathematics,
Formal Abstracts, linguistic processing of mathematics/science, modern AI and
big-data methods, and several sessions with contributed talks. The focused
sessions will be based on invited talks and discussion oriented.

CONFIRMED PARTICIPANTS/SPEAKERS (TBC)

João Araújo, Universidade Nova de Lisboa
Kevin Buzzard, Imperial College London
Michael R. Douglas*, Stony Brook University
Vlad Firoiu, DeepMind
Ben Goertzel, SingularityNET
Georges Gonthier, INRIA
Thomas C. Hales, University of Pittsburgh
John Harrison, Amazon
Sean Holden, University of Cambridge
Mikoláš Janota, University of Lisbon
Michael Kinyon, University of Denver
Joao Marques Silva, ANITI, University of Toulouse
David McAllester, Toyota Technological Institute at Chicago
Tomáš Mikolov, Facebook AI Research
Lawrence C. Paulson, University of Cambridge
Alison Pease, University of Dundee
Markus Rabe, Google Research
Stephan Schulz, DHBW Stuttgart
Daniel Selsam, Microsoft Research
Martin Suda, Czech Technical University in Prague
Robert Veroff, University of New Mexico
Petr Vojtchovsky, University of Denver
*: To be confirmed.


CONTRIBUTED TALKS
We solicit contributed talks. Selection of those will be based on extended
abstracts/short papers of 2 pages formatted with easychair.cls. Submission is
via EasyChair (https://easychair.org/conferences/?conf=aitp2020).

DATES
Submission deadline: December 3, 2019
Author notification: January 10, 2020
Conference registration: January 21, 2020
Camera-ready versions: March 1, 2020
Conference: March 22 - 27, 2020

POST-PROCEEDINGS
We will consider an open call for post-proceedings in an established series of
conference proceedings (LIPIcs, EPiC, JMLR) or a journal (AICom, JAR, JAIR).

PROGRAM COMMITTEE (TBC)

Jasmin Christian Blanchette, INRIA Nancy
Ulrich Furbach, University of Koblenz
Tibault Gauthier, Czech Technical University in Prague
Thomas C. Hales (co-chair), University of Pittsburgh
Sean Holden, University of Cambridge
Mikoláš Janota, University of Lisbon
Cezary Kaliszyk (co-chair), University of Innsbruck
Peter Koepke, University of Bonn
Konstantin Korovin, The University of Manchester
Ramana Kumar (co-chair), DeepMind
Sarah Loos, Google Research
Stephan Schulz (co-chair), DHBW Stuttgart
Geoff Sutcliffe, University of Miami
Josef Urban (co-chair), Czech Technical University in Prague
Sarah Winkler, University of Innsbruck


LOCATION AND PRICE

The conference will take place from March 22 to March 27 2020 in the CNRS
Paul-Langevin Conference Center
(https://www.caes.cnrs.fr/sejours/centre-paul-langevin/) located in the
mountain village of Aussois in Savoy. Dominated by the "Dent Parrachee", one
of the highest peaks of La Vanoise, Aussois is located on a sunny plateau at
1500 m altitude, offering a magnificent panorama of the surrounding mountains
and a direct access to the downhill ski slopes or cross country slopes in
winter. The total price for accommodation, food and registration for the five
days will be around 600 EUR.

ARRIVAL/DEPARTURE
Aussois is less than 2h from the airports of Lyon, Geneve, Chambery, Annecy,
Grenoble and Turin. There are trains and buses from these airports. Aussois is
7km from the Modane TGV station with direct trains from/to Paris. We will
organize a bus for the participants from there to Aussois. Further buses to
these airports/station can be found at http://www.altibus.com/ .


ORGANIZERS
Cezary Kaliszyk and Josef Urban

2019-10-14

[Caml-list] IJCAR 2020 - Call for Papers

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

IJCAR 2020
The 10th International Joint Conference on Automated Reasoning
Paris, France, June 29-July 5, 2020
https://ijcar2020.org

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


IJCAR is the premier international joint conference on all topics in automated
reasoning. The IJCAR 2020 technical program will consist of presentations of
high-quality original research papers, short papers describing interesting work
in progress, system descriptions, and invited talks. IJCAR 2020 (+ workshops,
tutorials, etc.) will take place in Paris (France) from June 29 to July 5 2020.
It will be co-located with the conference FSCD.

IJCAR 2020 is the merger of leading events in automated reasoning:
* CADE (Conference on Automated Deduction)
* FroCoS (Symposium on Frontiers of Combining Systems)
* ITP (International Conference on Interactive Theorem Proving)
* TABLEAUX (Conference on Analytic Tableaux and Related Methods)

TOPICS
======

IJCAR 2020 invites submissions related to all aspects of automated or
interactive reasoning, including foundations, implementations, and
applications. Original research papers and descriptions of working automated
deduction systems or proof assistants are solicited.

IJCAR topics include the following ones:

* Logics of interest include: propositional, first-order, classical,
equational, higher-order, non-classical, constructive, modal, temporal,
many-valued, substructural, description, type theory.

* Methods of interest include: tableaux, sequent calculi, resolution, model-
elimination, inverse method, paramodulation, term rewriting, induction,
unification, constraint solving, decision procedures, model generation,
model checking, semantic guidance, interactive theorem proving, logical
frameworks, AI-related methods for deductive systems, proof presentation,
automated theorem proving, combination of decision or proof procedures, SAT
and SMT solving, integration of proof assistants with automated provers and
other symbolic tools, etc.

* Applications of interest include: verification, formal methods, program
analysis and synthesis, computer mathematics, declarative programming,
deductive databases, knowledge representation, education, formalization of
mathematics etc.

The proceedings of IJCAR 2020 will be published by Springer in the LNAI/LNCS
series (www.springer.com/lncs).


IMPORTANT DATES
===============

* Abstract submission: January 16, 2020
* Paper submission: January 23, 2020
* Rebuttal: March 6-10, 2020
* Notification: March 20, 2020
* Final version of papers due: April 10, 2020
* IJCAR Conference + Workshops: June 29 - July 5, 2020


SUBMISSION GUIDELINES
=====================

Submission is electronic, through
https://easychair.org/conferences/?conf=ijcar2020

Authors are strongly encouraged to use LaTeX and the Springer "llncs" format,
which can be obtained from
http://www.springer.de/comp/lncs/authors.html

We solicit three categories of submissions:

REGULAR PAPERS.
Submissions, not exceeding fifteen (15) pages excluding bibliography, should
contain original research, and sufficient detail to assess the merits and
relevance of the contribution. For papers reporting experimental results,
authors are strongly encouraged to make their data and software available with
their submission for reproducibility. In particular submissions describing
formal proofs are expected to be accompanied by the source files of the
formalization. The PC will take availability of software and data into account
when evaluating submissions. Submissions reporting on case studies in an
industrial context are strongly invited, and should describe details,
weaknesses and strength in sufficient depth. Simultaneous submission to other
conferences with proceedings or submission of material that has already been
published elsewhere is not allowed.

SYSTEM DESCRIPTIONS.
Submissions, not exceeding seven (7) pages excluding bibliography, should
describe the implemented tool and its novel features. Submissions in this
category should bear the phrase "(system description)" beneath the title. One
author is expected to be able to perform a demonstration on demand to accompany
a tool presentation. Papers describing tools that have already been presented
in other conferences before will be accepted only if significant and clear
enhancements to the tool are reported and implemented.

SHORT PAPERS.
Submissions, not exceeding five (5) pages excluding bibliography, and
describing interesting work in progress. Such a preliminary report may consist
of an extended abstract. Each of these papers should bear the phrase "(short
paper)" beneath the title. Accepted submissions in this category will be
presented as short talks and published in the main proceedings. There will be
no downgrading from regular papers or system descriptions to short papers.


All submissions should meet high academic standards; proofs of theoretical
results that do not fit in the page limit, executables of systems, and input
data of experiments should be made available, via a reference to a website or
in an appendix of the paper.


BEST PAPER AWARD
================

IJCAR 2020 will recognize the most outstanding submission with a best paper
award at the conference.


STUDENT TRAVEL AWARDS
====================

Woody Bledsoe Travel Awards will be available to support selected students
attending the conference.


SPECIAL ISSUE
=============

The authors of a selection of the best IJCAR 2020 papers will be invited to
submit an extended version of their paper after the conference, to be published
in a special issue of Logical Methods in Computer Science.


ORGANIZATION
============

Conference Chair:
* Kaustuv Chaudhuri (INRIA, Ecole Polytechnique)

Programme Chairs:
* Nicolas Peltier (CNRS, LIG, Univ. Grenoble Alpes, Grenoble France),
* Viorica Sofronie-Stokkermans (University Koblenz-Landau, Koblenz, Germany)

Workshop, Tutorial and Competition Chairs:
* Giulio Manzonetto (Université Paris-Nord, France)
* Andrew Reynolds (University of Iowa, USA)

Programme Committee:
* Takahito Aoto (Niigata University, Japan)
* Carlos Areces (FaMAF Universidad Nacional de Cordoba, Argentina)
* Jeremy Avigad (Carnegie Mellon University, USA)
* Franz Baader (TU Dresden, Germany)
* Peter Baumgartner (Data 61 and CSIRO, Australia)
* Christoph Benzmüller (Freie Universität Berlin, Germany)
* Armin Biere (Johannes Kepler University Linz, Austria)
* Nikolaj Bjorner (Microsoft Research, USA)
* Jasmin Blanchette (Vrije Universiteit Amsterdam, Netherlands)
* Maria Paola Bonacina (Universita degli Studi di Verona, Italy)
* James Brotherston (University College London, UK)
* Serenella Cerrito (IBISC, Univ. Evry, Paris Saclay University, France)
* Agata Ciabattoni (Vienna University of Technology, Austria)
* Koen Claessen (Chalmers University of Technology, Gothenburg, Sweden)
* Leonardo de Moura (Microsoft Research, USA)
* Stéphane Demri (CNRS, LSV, ENS Paris-Saclay, France)
* Gilles Dowek (Inria and ENS Paris-Saclay, France)
* Marcelo Finger (University of São Paulo, Brazil)
* Pascal Fontaine (Universite de Lorraine, CNRS, Inria, LORIA, France)
* Didier Galmiche (Universite de Lorraine - LORIA, France)
* Silvio Ghilardi (Universita degli Studi di Milano, Italy)
* Martin Giese (Universitetet i Oslo, Norway)
* Juergen Giesl (RWTH Aachen University, Germany)
* Valentin Goranko (Stockholm University, Sweden)
* Rajeev Gore (The Australian National University, Australia)
* Stefan Hetzl (Vienna University of Technology, Austria)
* Marijn J. H. Heule (The University of Texas at Austin, USA)
* Cezary Kaliszyk (University of Innsbruck, Austria)
* Deepak Kapur (University of New Mexico, USA)
* Laura Kovacs (Vienna University of Technology, Austria)
* Christopher Lynch (Clarkson University, USA)
* Assia Mahboubi (Inria, France)
* Panagiotis Manolios (Northeastern University, USA)
* Dale Miller (Inria and LIX/Ecole Polytechnique, France)
* Claudia Nalon (University of Brasilia, Brazil)
* Tobias Nipkow (Technical University of Munich, Germany)
* Albert Oliveras (Universitat Politècnica de Catalunya, Spain)
* Jens Otten (University of Oslo, Norway)
* Lawrence Paulson (University of Cambridge, UK)
* Frank Pfenning (Carnegie Mellon University, USA)
* Andrei Popescu (Middlesex University London, UK)
* Andrew Reynolds (University of Iowa, USA)
* Christophe Ringeissen (LORIA-INRIA, France)
* Katsuhiko Sano (Hokkaido University, Japan)
* Renate Schmidt (The University of Manchester, UK)
* Stephan Schulz (DHBW Stuttgart, Germany)
* Roberto Sebastiani (DISI, University of Trento, Italy)
* Martin Suda (Czech Technical University, Czech Republic)
* Geoff Sutcliffe (University of Miami, USA)
* Sofiene Tahar (Concordia University, Canada)
* Cesare Tinelli (The University of Iowa, USA)
* Christian Urban (King's College London, UK)
* Josef Urban (Czech Technical University in Prague, Czech Republic)
* Uwe Waldmann (Max Planck Institute for Informatics, Germany)
* Christoph Weidenbach (Max Planck Institute for Informatics, Germany)