[Hol-info] [ICLP 2017] Final Call for Papers

[Tommaso.Urli]

Apologies for double-posting.

 DEADLINE FOR ABSTRACT EXTENDED TO April 26  ***
 PAPER SUBMISSION DEADLINE May 2 ***

ICLP 2017 Call for Papers
-

The 33rd International Conference on Logic Programming (ICLP 2017)
will take place in Melbourne, Australia alongside SAT 2017 and CP 2017,
from August 28th to September 1st, 2017 which is the week immediately
following IJCAI 2017.

Full information at http://iclp17.a4lp.org
Call for Papers at http://iclp17.a4lp.org/call_for_papers.html

Conference Scope


Since the first conference held in Marseille in 1982, ICLP has been
the premier international conference for presenting research in logic
programming. Contributions are sought in all areas of logic
programming, including but not restricted to:

 - Theory: Semantic Foundations, Formalisms, Nonmonotonic Reasoning,
   Knowledge Representation.

 - Implementation: Compilation, Virtual Machines, Parallelism,
   Constraint Handling Rules, Tabling.

 - Environments: Program Analysis, Transformation, Validation,
   Verification, Debugging, Profiling, Testing.

 - Language Issues: Concurrency, Objects, Coordination, Mobility,
   Higher Order, Types, Modes, Assertions, Programming Techniques.

 - Related Paradigms: Inductive and Co-inductive Logic Programming,
   Constraint Logic Programming, Answer-Set Programming, SAT-Checking.

 - Applications: Databases, Big Data, Data Integration and Federation,
   Software Engineering, Natural Language Processing, Web and Semantic
   Web, Agents, Artificial Intelligence, Bioinformatics, and
   Education.

In addition to the presentations of accepted papers, the technical
program will include invited talks, advanced tutorials, the doctoral
consortium, and several workshops.


Important Dates
-

- Registration (abstract):  26 April, 2017
- Paper submission:  2 May,   2017
- Notification:  6 June,  2017
- Revision submission (TPLP only):  20 June,  2017
- Final notifications:   4 July,  2017
- Camera-ready copy:18 July, 2017
- Conference:   28 Aug / 1 Sep, 2017


Submission Details
--

All submissions must be made via the EasyChair conference system
(http://www.easychair.org/conferences/?conf=iclp2017). Submissions of
regular papers (RPs) must follow the condensed TPLP format (template
available from ICLP’s web page) and not exceed 14 pages including
bibliography. RPs may be supplemented with appendices for proofs and
details of datasets which do not count towards the page limit and
which will be available as appendices to the published paper. Three
kinds of RPs will be accepted:

 * Technical papers for technically sound, innovative ideas that can
   advance the state of logic programming;

 * Application papers that impact interesting application domains;

 * System and tool papers which emphasize novelty, practicality,
   usability, and availability of the systems and tools described.

Application, system, and tool papers need to be clearly marked in
their title.

All submissions must be written in English and describe original,
previously unpublished research, and must not simultaneously be
submitted for publication elsewhere. These restrictions do not apply
to previously accepted workshop papers with a limited audience and/or
without archival proceedings.

Papers of the highest quality will be selected to be published in the
journal of Theory and Practice of Logic Programming (TPLP), Cambridge
University Press (CUP). In order to ensure the quality of the final
version, papers may be subject to more than one round of refereeing
(within the decision period).

The program committee may recommend some RPs to be published as
Technical Communications (TCs). TCs will be published by Dagstuhl
Publishing in the OpenAccess Series in Informatics (OASIcs). TCs must
follow the OASIcs format (template available from ICLP’s web page) and
not exceed 14 pages excluding the bibliography and a short appendix
(up to 5 more pages). TC’s authors can also elect to convert their
submissions into extended abstracts, of 2 or 3 pages, for inclusion in
the OASIcs proceedings. This should allow authors to submit a long
version elsewhere.

All RPs and TCs will be presented during the conference. Authors of
accepted papers will, by default, be automatically included in the
list of ALP members, who will receive quarterly updates from the Logic
Programming Newsletter at no cost.


Conference Organization
---

General Chairs:
- Maria Garcia de la Banda   Monash University, Australia
- Guido Tack Monash University, Australia

Program Chairs:
- Ricardo Rocha  University of Porto, Portugal
- Tran Cao Son   New Mexico State University, USA

Workshop Chair:
- Enrico PontelliNew Mexico 

[Hol-info] FroCoS 2017 DEADLINE EXTENSION

[Cláudia Nalon]

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

*** DEADLINE EXTENSION ***

   FINAL CALL FOR PAPERS

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


New Submission Deadlines: 1st May (abstracts), 5th May (full papers)

Due  to several  requests, we  are extending  the deadline.   These
dates  are final.


GENERAL INFORMATION
   The 11th International Symposium on Frontiers of Combining Systems
   (FroCoS 2017) will be held in Brasilia, Brazil, between September 27 
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
   João 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 Bimbó (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 São 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 in total, including references and figures.

   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
   

[Hol-info] SMT 2017 workshop : 2nd CFP, Deadline 1st/8th May

[Martin Nyx Brain]

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

--- Call For Papers ---

SMT 2017
15th International Workshop on Satisfiability Modulo Theories
July 22 - 23, 2017, Heidelberg, Germany
Affiliated with CAV 2017

==

Background
--

Determining the satisfiability of first-order formulas modulo
background theories, known as the Satisfiability Modulo Theories (SMT)
problem, has proved to be an enabling technology for verification,
synthesis, test generation, compiler optimization, scheduling, and
other areas. The success of SMT techniques depends on the development
of both domain-specific decision procedures for each background theory
(e.g., linear arithmetic, the theory of arrays, or the theory of
bit-vectors) and combination methods that allow one to obtain more
versatile SMT tools. These ingredients together make SMT techniques
well-suited for use in larger automated reasoning and verification
efforts.

Aims and Scope
--

The aim of the workshop is to bring together researchers and users of
SMT tools and techniques. Relevant topics include but are not limited
to:

* Decision procedures and theories of interest
* Combinations of decision procedures
* Novel implementation techniques
* Applications and case studies
* Benchmarks and evaluation methodologies
* Theoretical results

Papers on pragmatic aspects of implementing and using SMT tools, as
well as novel applications of SMT, are especially encouraged.

Important dates
---

* Abstract submission deadline: Mon, May 1, 2017
* Paper submission deadline: Mon, May 8, 2017
* Notification: Mon, Jun 5, 2017
* Camera ready versions due: Mon, Jun 12, 2017
* Workshop: July 22-23, 2017

Paper submission and Proceedings


Three categories of submissions are invited:

* Extended abstracts: given the informal style of the workshop, we
strongly encourage the submission of preliminary reports of work in
progress. They may range in length from very short (a couple of pages)
to the full 10 pages and they will be judged based on the expected
level of interest for the SMT community. They will be included in the
informal proceedings.

* Original papers: contain original research (simultaneous submissions
are not allowed) and sufficient detail to assess the merits and
relevance of the submission. For papers reporting experimental results,
authors are strongly encouraged to make their data available.

* Presentation-only papers: describe work recently published or
submitted and will not be included in the proceedings. We see this as a
way to provide additional access to important developments that SMT
Workshop attendees may be unaware of.

Papers in all three categories will be peer-reviewed. Papers should
not exceed 10 pages and should be in standard-conforming
PDF. Technical details may be included in an appendix to be read at
the reviewers' discretion. Final versions should be prepared in LaTeX
using the easychair.cls class file. (The 10 page does not include
references.)

To submit a paper, go to the EasyChair SMT page
 and follow the
instructions there.

Program Committee Chairs
-

Liana Hadarean (Synopsys)
Martin Brain (Oxford University)


Program Committee
-

Alberto Griggio (Fondazione Bruno Kessler - FBK)
Aina Niemetz (Johannes Kepler University)
Bruno Dutertre (SRI International)
Pascal Fontaine (Université de Lorraine)
Christoph M. Wintersteiger (Microsoft Research)
Jochen Hoenicke (University of Freiburg)
Guy Katz (Stanford University)
Sylvain Conchon (Laboratoire de Recherche en Informatique - LRI)
Mate Soos (Gotham Digital Science)
Alexander Nadel (Intel)
Jasmin Christian Blanchette (Vrije Universiteit Amsterdam)
Sicun Gao (MIT)
Rayna Dimitrova (Max Planck Institute for Software Systems)
Florian Schanda (Altran)




--
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] CPP 2018 Call for papers

[Amy Felty]

 CALL FOR PAPERS

The 7th ACM SIGPLAN International Conference
 on Certified Programs and Proofs (CPP 2018)

 co-located with POPL 2018
   in cooperation with ACM SIGLOG

   http://popl18.sigplan.org/track/CPP-2018

  8-9 January, 2018, Los Angeles, USA


Certified Programs and Proofs (CPP) is an international forum on
theoretical and practical topics in all areas, including computer
science, mathematics, and education, that consider certification as an
essential paradigm for their work. Certification here means formal,
mechanized verification of some sort, preferably with production of
independently checkable certificates.

Important dates
---
  - Abstract submission deadline:   Fri 6 Oct 2017
  - Full paper submission deadline: Wed 11 Oct 2017
  - Notification:   Tue 14 Nov 2017
  - Camera-ready deadline:  Fri 24 Nov 2017
  - Conference dates:   Mon 8 - Tue 9 Jan 2018

Topics of interest
--
We welcome submissions in research areas related to formal
certification of programs and proofs. The following is a suggested
list of topics of interests to CPP. This is a non-exhaustive list and
should be read as a guideline rather than a requirement.

  - certified or certifying programming, compilation, linking, OS
kernels, runtime systems, and security monitors;
  - program logics, type systems, and semantics for certified code;
  - certified decision procedures, mathematical libraries, and
mathematical theorems;
  - proof assistants and proof theory;
  - new languages and tools for certified programming;
  - program analysis, program verification, and proof-carrying code;
  - certified secure protocols and transactions;
  - certificates for decision procedures, including linear algebra,
polynomial systems, SAT, SMT, and unification in algebras of
interest;
  - certificates for semi-decision procedures, including equality,
first-order logic, and higher-order unification;
  - certificates for program termination;
  - logics for certifying concurrent and distributed programs;
  - higher-order logics, logical systems, separation logics, and logics
for security;
  - teaching mathematics and computer science with proof assistants.

Submission Guidelines
-

Papers should be submitted in PDF format through the EasyChair
submission page at

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

Submitted papers must be formatted following the ACM SIGPLAN
Proceedings format using the sigplanconf format (not the acmart
format), using 10 point font for the main text (not the default 9pt
font).

   http://www.sigplan.org/Resources/Author/

Submitted papers should not exceed 12 pages, including tables and
figures, but excluding bibliography. Shorter papers are welcome and
will be given equal consideration.

Abstracts must be submitted by October 6, 2017 (AOE). The deadline for
full papers is October 11, 2017 (AOE), and authors have the option to
withdraw their papers during the window between the two.

Submissions must be written in English and provide sufficient detail
to allow the program committee to assess the merits of the paper. They
should begin with a succinct statement of the issues, a summary of the
main results, and a brief explanation of their significance and
relevance to the conference, all phrased for the
non-specialist. Technical and formal developments directed to the
specialist should follow. References and comparisons with related work
should be included. Papers not conforming to the above requirements
concerning format and length may be rejected without further
consideration.

Whenever appropriate, the submission should come along with a formal
development, using whatever prover, e.g., Agda, Coq, Dafny, Elf, HOL,
HOL-Light, Isabelle, Lean, Matita, Mizar, NQTHM, PVS, Vampire,
etc. Such formal developments must be submitted together with the
paper as auxiliary material, and will be taken into account during the
reviewing process.

The results must be unpublished and not submitted for publication
elsewhere, including the proceedings of other published conferences or
workshops. The PC chairs should be informed of closely related work
submitted to a conference or journal in advance of
submission. Original formal proofs of known results in mathematics or
computer science are welcome. One author of each accepted paper is
expected to present it at the conference.

For any questions about the formatting or submission of papers, please
consult the PC chairs.

Program Committee
-
  Reynald Affeldt (AIST, Japan)
  June Andronick (Data61, CSIRO and UNSW, Australia), co-chair
  Lennart Beringer (Princeton University, USA)
  Jasmin Blanchette (Vrije Universiteit Amsterdam, Netherlands)
  Sandrine Blazy (University of Rennes 1, France)
  Sylvie Boldo (Inria and Université Paris-Saclay, France)
  James Cheney (University of Edinburgh, UK)
  Amy