Warning: deadline on September 27, 2021
Call for Workshops - FLoC 2022 — The 2022 Federated Logic Conference
July 31 - August 12, 2022
Haifa, Israel
http://www.floc2022.org/
CALL FOR WORKSHOPS
The Eighth Federated Logic Conference (FLoC 2022) will host ten
conferences including
LICS (37th Annual ACM/IEEE Symposium on Logic in Computer Science) https://lics.siglog.org/
Workshop chair: Frederic Blanqui Frederic.Blanqui(a)inria.fr
SUBMISSION OF WORKSHOP PROPOSALS
Researchers and practitioners are invited to submit proposals for workshops on
topics in the field of computer science, related to logic in the broad sense.
Each workshop proposal must indicate one affiliated conference of FLoC 2022.
It is strongly suggested that prospective workshop organizers contact the
relevant conference workshop chair before submitting a proposal.
Each proposal should consist of the following two parts.
1) A short scientific justification of the proposed topic, its significance,
and the particular benefits of the workshop to the community, as well as a
list of previous or related workshops (if relevant).
2) An organisational part including:
- contact information for the workshop organizers;
- proposed affiliated conference;
- estimate of the number of workshop participants (please note that small workshops, i.e., of less than ~13 participants, will likely be cancelled or merged);
- proposed format and agenda (e.g. paper presentations, tutorials, demo sessions, etc.);
- potential invited speakers (note that expenses of workshop invited speakers are not covered by FLoC);
- procedures for selecting papers and participants;
- plans for dissemination, if any (e.g. a journal special issue);
- duration (which may vary from one day to two days);
- preferred period (pre or post FLoC);
- virtual/hybrid backup plans (including platform preference).
The FLoC Organizing Committee will determine the final list of accepted
workshops based on the recommendations from the Workshop Chairs of the hosting
conferences and availability of space and facilities.
Proposals should be submitted through EasyChair:
https://easychair.org/conferences/?conf=floc2022workshops
Please see the Workshop Guidelines page: https://floc2022.org/workshops/ for further details and FAQ.
IMPORTANT DATES
Submission of workshop proposals deadline: September 27, 2021 (note extended deadline)
Notification: November 1, 2021
Pre-FLoC workshops: Sunday & Monday, July 31–August 1, 2022 (note corrected dates)
Post-FLoC workshops: Thursday & Friday, August 11-12, 2022
CONTACT INFORMATION
Questions regarding proposals should be sent to the workshop chairs of the
proposed affiliated conference. General questions should be sent to:
shaull(a)technion.ac.il
GuillermoAlberto.Perez(a)uantwerpen.be
FLoC 2022 WORKSHOP CHAIRS
Shaull Almagor
Guillermo A. Perez
***Apologies for multiple receptions of this message***
First Call for Workshops - ICALP 2022 -
July 4 - July 8, 2022
Paris, France
https://icalp2022.irif.fr/ <https://icalp2022.irif.fr/>
The International Colloquium on Automata, Languages and Programming (ICALP) is the main conference and annual meeting of the EATCS (European Association for Theoretical Computer Science). This year, after two virtual ICALP events, we are happy to be able to host this event in hybrid mode--and hope that many of us will be able to meet again in beautiful Paris! This is a call for workshops to be affiliated with ICALP 2022. We invite researchers to organise workshops on central topics on Automata, Languages and Programming, to help further mark off ICALP 2022.
Important Dates:
Workshop proposal deadline: Friday 19 November 2021, 23:59 AoE
Workshop notification: Friday 10 December 2021
Workshops: Monday 4 July 2022.
We strongly suggest that prospective workshop organizers contact the workshop selection committee before submitting a proposal.
Workshop Proposal Guidelines:
Proposals should be submitted no later than
*** Friday 19 November 2021 ***
by sending an email to the workshop selection committee, see below. You should expect notification on the acceptance of your proposal by 10 December 2021.
A workshop proposal submission should consist of the following
A short scientific justification of the proposed topic, its significance, and the particular benefits of the workshop to the community.
An organisational part including:
- workshop’s name and URL (if already available);
- contact information for the workshop organizers (including their webpages);
- expected number of participants (if available, please include the data of previous years);
- proposed format and agenda (e.g. paper presentations, tutorials, see below for more details);
- potential invited speakers;
- plans for dissemination, if any (e.g. a journal special issue);
- planned format of the event (see below for mode details);
- virtual/hybrid backup plans (including platform preference).
As for the format, a standard option is a full one-day workshop consisting of invited talks by leading experts and of shorter contributed talks, either directly invited by the organizers or selected among presentation submissions. Deviations from this standard are also welcome, including open problem sessions, discussion panels, or working sessions. If you plan to have invited speakers, please specify their expected number and, if possible, tentative names. If you plan a call for contributed talks (or papers) followed by a selection procedure, the submission date should be scheduled after ICALP 2022 notification (11 April 2022), while the notification should take place before the early registration deadline. In your submission please include details on the schedule, planned procedure of selecting contributed talks (or papers). If you plan to have published proceedings of your workshop, please provide the name of the publisher.
Note that ICALP 2022 is not able to provide financial support for the organization of workshops. The conference can however provide a room, internet connection and help with some local organisation. For workshops that are online or in hybrid mode, it is expected that the organizers provide the supporting technical infrastructure.
Workshop Selection Committee:
Track A: Valia Mitsou <vmitsou(a)irif.fr <mailto:vmitsou@irif.fr>>
Track B: Mahsa Shirmohammadi <mahsa(a)irif.fr <mailto:mahsa@irif.fr>>
Final Call for Workshops - FLoC 2022 — The 2022 Federated Logic Conference
July 31 - August 12, 2022
Haifa, Israel
http://www.floc2022.org/
CALL FOR WORKSHOPS
The Eighth Federated Logic Conference (FLoC 2022) will host the following
ten
conferences and affiliated workshops.
LICS (37th Annual ACM/IEEE Symposium on Logic in Computer Science)
http://lics.rwth-aachen.de/
Workshop chair: Frederic Blanqui Frederic.Blanqui(a)inria.fr
FSCD (7th International Conference on Formal Structures for Computation and
Deduction)
http://fscd-conference.org/
Workshop chair: Nachum Dershowitz nachumd(a)tau.ac.il
ITP (13th International Conference on Interactive Theorem Proving)
https://itp-conference.github.io/
Workshop chair: Cyril Cohen cyril.cohen(a)inria.fr
IJCAR (International Joint Conference on Automated Reasoning)
http://www.ijcar.org
Workshop chairs: Sophie Tourret stourret(a)mpi-inf.mpg.de and Simon Robillard
CSF (35th IEEE Computer Security Foundations Symposium)
http://www.ieee-security.org/CSFWweb/
Workshop chair: Musard Balliu musard(a)kth.se
CAV (34th International Conference on Computer Aided Verification)
http://i-cav.org/
Workshop chair: Grigory Fedyukovich grigory(a)cs.fsu.edu
KR (19th International Conference on Principles of Knowledge Representation
and Reasoning)
http://www.kr.org/
Workshop chair: Stefan Borgwardt stefan.borgwardt(a)tu-dresden.de
ICLP (38th International Conference on Logic Programming)
https://www.cs.nmsu.edu/ALP/conferences/
Workshop chair: Daniela Inclezan inclezd(a)miamioh.edu
SAT (25th International Conference on Theory and Applications of
Satisfiability Testing)
http://www.satisfiability.org
Workshop chair: Alexander Nadel alexander.nadel(a)intel.com
CP (25th International Conference on Principles and Practice of Constraint
Programming)
http://a4cp.org/events/cp-conference-series
Workshop chair: Ciaran McCreesh ciaran.mccreesh(a)glasgow.ac.uk
SUBMISSION OF WORKSHOP PROPOSALS
Researchers and practitioners are invited to submit proposals for workshops
on
topics in the field of computer science, related to logic in the broad
sense.
Each workshop proposal must indicate one affiliated conference of FLoC 2022.
It is strongly suggested that prospective workshop organizers contact the
relevant conference workshop chair before submitting a proposal.
Each proposal should consist of the following two parts.
1) A short scientific justification of the proposed topic, its significance,
and the particular benefits of the workshop to the community, as well as a
list of previous or related workshops (if relevant).
2) An organisational part including:
- contact information for the workshop organizers;
- proposed affiliated conference;
- estimate of the number of workshop participants (please note that small
workshops, i.e., of less than ~13 participants, will likely be cancelled or
merged);
- proposed format and agenda (e.g. paper presentations, tutorials, demo
sessions, etc.);
- potential invited speakers (note that expenses of workshop invited
speakers are not covered by FLoC);
- procedures for selecting papers and participants;
- plans for dissemination, if any (e.g. a journal special issue);
- duration (which may vary from one day to two days);
- preferred period (pre or post FLoC);
- virtual/hybrid backup plans (including platform preference).
The FLoC Organizing Committee will determine the final list of accepted
workshops based on the recommendations from the Workshop Chairs of the
hosting
conferences and availability of space and facilities.
Proposals should be submitted through EasyChair:
https://easychair.org/conferences/?conf=floc2022workshops
Please see the Workshop Guidelines page: https://floc2022.org/workshops/
for further details and FAQ.
IMPORTANT DATES
Submission of workshop proposals deadline: September 27, 2021
Notification: November 1, 2021
Pre-FLoC workshops: Sunday & Monday, July 31–August 1, 2022
Post-FLoC workshops: Thursday & Friday, August 11-12, 2022
CONTACT INFORMATION
Questions regarding proposals should be sent to the workshop chairs of the
proposed affiliated conference. General questions should be sent to:
shaull(a)technion.ac.il
GuillermoAlberto.Perez(a)uantwerpen.be
FLoC 2022 WORKSHOP CHAIRS
Shaull Almagor
Guillermo A. Perez
Join the Logica Universalis Webinar!
The next session will be held on Wednesday, September 15 at 4pm CEST with the talk
Mathematical Perspectives on Liar Paradoxes<https://link.springer.com/article/10.1007/s11787-021-00277-2>
Josué Antonio Nescolarde Selva<https://urldefense.proofpoint.com/v2/url?u=https-3A__josuenescolardeselva.w…> (University of Alicante, Spain)
Chair: Maria Manzano<https://urldefense.proofpoint.com/v2/url?u=https-3A__en.wikipedia.org_wiki_…>, Editorial Board LU
Associate Organization Spanish Society of Logic and Methodology and Philosophy of Science<https://urldefense.proofpoint.com/v2/url?u=https-3A__www.solofici.org_&d=Dw…>
presented by its president Cristina Corredor<https://urldefense.proofpoint.com/v2/url?u=https-3A__epimenides.usal.es_-3F…>
The Logica Universalis Webinar is a World Seminar Series connected to the journal Logica Universalis<https://www.springer.com/journal/11787/>, the book series Studies in Universal Logic<https://www.springer.com/series/7391> and the Universal Logic Project<https://logica-universalis.org/>. It is an open platform for all scholars interested in the many aspects of logic. (See the full program here<https://www.springer.com/journal/11787/updates/18988758>.)
The sessions take place on Wednesdays at 4pm CEST (click here<https://www.timeanddate.com/worldclock/fixedtime.html?msg=Logica+Universali…> to convert to your timezone). They are held via Zoom and are free to attend. Please register in advance.
Registration is now open!<https://springer.zoom.us/meeting/register/tJMvdu6vrzMiHda_iDhjxw9vA9d7we9gT…>
Each session of the webinar is chaired by a member of the editorial board of the journal Logica Universalis (LU), the book series Studies in Universal Logic (SUL) or an organizer of an event of the Universal Logic Project (ULP). Sessions will start with a short presentation of a logical organization related to the region of the speaker or the topic of the talk. The talk (30 min) will focus on a recently published paper in LU, on a book in SUL, on an event or on the ULP. Talks are followed by a discussion (15 min).
Video recordings of the seminars are uploaded on the YouTube channel Universal Logic Project<https://www.youtube.com/channel/UCPS1c5ApuwjuCV9UjXHUN4w>.
---
To unsubscribe from these notifications for the Logica Universalis Webinar please send a message with 'Unsubscribe' to this e-mail address (antje.herbst(a)springernature.com<mailto:antje.herbst@springernature.com>).
--
Antje Herbst
Associate Editor Mathematics
Journals
Springer Nature
Tiergartenstraße 17, 69121 Heidelberg, Germany
T +49 62214878984
antje.herbst(a)springernature.com<mailto:antje.herbst@springernature.com>
www.springernature.com<http://www.springernature.com/>
--
Springer Nature is a leading research, educational and professional publisher, providing quality content to our communities through a range of innovative platforms, products and services. Every day, around the globe, our imprints, books, journals and resources reach millions of people - helping researchers, students, teachers & professionals to discover, learn and achieve.
--
Branch of Springer-Verlag GmbH, Heidelberger Platz 3, 14197 Berlin, Germany
Registered Office: Berlin / Amtsgericht Berlin-Charlottenburg, HRB 91881 B
Directors: Martin Mos, Dr. Ulrich Vest, Dr. Niels Peter Thomas
- Application deadline: Midnight, 17 Oct 2021
- Starting date: As soon as possible after Oct 1
- Salary: £35,931-£37,979
- Duration: until February 2023
Applications are invited for the post of Post-Doctoral Research Assistant in the Computer Science Department at Royal Holloway, University of London.
Successful applicants will be working on the EPSRC-funded "Verification of Hardware Concurrency via Model Learning" (CLeVer) project (EP/S028641/1), led by Alexandra Silva (UCL) and Matteo Sammartino (Royal Holloway, University of London).
This is a joint research effort involving Royal Holloway University of London, University College London, and ARM, world-leading designer of multi-core chips.
For an informal discussion about the post, please contact Dr. Matteo Sammartino on matteo.sammartino(a)rhul.ac.uk.
# Project Description
Digital devices increasingly rely on multi-threaded computation, with sophisticated concurrent behaviour becoming prevalent at any scale. As the complexity of these systems increases, there is a pressing need to automate the assessment of their correctness, especially with respect to concurrency-related aspects. Formal verification provides highly effective techniques to assess the correctness of systems. However, formal models are usually built by humans, and as such can be error-prone and inaccurate.
The CLeVer project aims to:
- develop a novel verification framework that relies on learning techniques to automatically build and verify models of concurrency, with a particular focus on multi-core systems.
- apply the framework to real-world verification tasks, in collaboration with ARM.
# The ideal candidate
We are looking for candidates with a PhD in one of the following areas: model-based testing and verification, formal methods for concurrency, automated analysis of hardware systems. Experience in multiple areas will be valued. Candidates ideally should also have strong programming skills.
# Where to apply
https://jobs.royalholloway.ac.uk/0721-259-R
Join the Logica Universalis Webinar!
The next session will be held on Wednesday, September 8 at 4pm CEST with the talk
Decidability of Logical Theories and Their Combination<https://www.springer.com/gp/book/9783030565534>
João Rasga<https://urldefense.proofpoint.com/v2/url?u=https-3A__fenix.tecnico.ulisboa.…> and Cristina Sernadas<https://urldefense.proofpoint.com/v2/url?u=https-3A__math.tecnico.ulisboa.p…> (Instituto Superior Técnico, Lisbon, Portugal)
Chair: Razvan Diaconescu<https://urldefense.proofpoint.com/v2/url?u=https-3A__rdiaconescu.weebly.com…>, Editorial Board SUL
Associate Organization: Security and Quantum Information Group<https://sqigmath.tecnico.ulisboa.pt/>
presented by its founder and coordinator Paulo Mateus<http://sqig.math.ist.utl.pt/pmat/>
The Logica Universalis Webinar is a World Seminar Series connected to the journal Logica Universalis<https://www.springer.com/journal/11787/>, the book series Studies in Universal Logic<https://www.springer.com/series/7391> and the Universal Logic Project<https://logica-universalis.org/>. It is an open platform for all scholars interested in the many aspects of logic. (See the full program here<https://www.springer.com/journal/11787/updates/18988758>.)
The sessions take place on Wednesdays at 4pm CEST (click here<https://www.timeanddate.com/worldclock/fixedtime.html?msg=Logica+Universali…> to convert to your timezone). They are held via Zoom and are free to attend. Please register in advance.
Registration is now open!<https://springer.zoom.us/meeting/register/tJMvdu6vrzMiHda_iDhjxw9vA9d7we9gT…>
Each session of the webinar is chaired by a member of the editorial board of the journal Logica Universalis (LU), the book series Studies in Universal Logic (SUL) or an organizer of an event of the Universal Logic Project (ULP). Sessions will start with a short presentation of a logical organization related to the region of the speaker or the topic of the talk. The talk (30 min) will focus on a recently published paper in LU, on a book in SUL, on an event or on the ULP. Talks are followed by a discussion (15 min).
Video recordings of the seminars are uploaded on the YouTube channel Universal Logic Project<https://www.youtube.com/channel/UCPS1c5ApuwjuCV9UjXHUN4w>.
---
To unsubscribe from these notifications for the Logica Universalis Webinar please send a message with 'Unsubscribe' to this e-mail address (antje.herbst(a)springernature.com<mailto:antje.herbst@springernature.com>).
--
Antje Herbst
Associate Editor Mathematics
Journals
Springer Nature
Tiergartenstraße 17, 69121 Heidelberg, Germany
T +49 62214878984
antje.herbst(a)springernature.com<mailto:antje.herbst@springernature.com>
www.springernature.com<http://www.springernature.com/>
--
Springer Nature is a leading research, educational and professional publisher, providing quality content to our communities through a range of innovative platforms, products and services. Every day, around the globe, our imprints, books, journals and resources reach millions of people - helping researchers, students, teachers & professionals to discover, learn and achieve.
--
Branch of Springer-Verlag GmbH, Heidelberger Platz 3, 14197 Berlin, Germany
Registered Office: Berlin / Amtsgericht Berlin-Charlottenburg, HRB 91881 B
Directors: Martin Mos, Dr. Ulrich Vest, Dr. Niels Peter Thomas
CALL FOR PARTICIPATION (onsite/online)
19th International Conference on
Relational and Algebraic Methods in Computer Science
RAMiCS 2021
2 to 5 November 2021, CIRM, Marseille, France
https://ramics19.lis-lab.fr/
IMPORTANT DATES:
Registration deadline: 12 September 2021
RAMiCS 2021: 2 to 5 November 2021
Since 1994, the RAMICS conference series has been the main venue for
research on relation algebras, Kleene algebras and similar algebraic
formalisms, and their applications as conceptual and methodological
tools in computer science and beyond.
RAMiCS 2021 will take place at CIRM, the Centre International de
Rencontres Mathématiques at the beautiful Luminy campus close to
Marseille. It will take the form of a hybrid conference, allowing
both onsite and online participation. Participation is free, but
subject to approval by the conference organisers. Please register at:
https://ramics19.lis-lab.fr/#registration
We strongly encourage participation on-site and remark that the CIRM
is a very pleasant place for a conference, but understand that some
participants will only be able to join online. Please register before
September 12, 2021. Note that after this date we might not be able to
ensure accommodation at the conference centre and that a late
registration fee might apply for online participation.
The RAMiCS 2021 program features 3 invited talks and 29 contributed
talks. For details, see
https://ramics19.lis-lab.fr/accepted.html
INVITED TALKS:
Marcelo Frias, Buenos Aires Institute of Technology, Argentina
Relational Tight Field Bounds for Distributed Analysis of Programs
Barbara König, Duisburg-Essen University, Germany
Fixpoint Games
Dmitriy Zhuk, Lomonosov Moscow State University, Russia
Quantified Constraint Satisfaction Problem: towards the
classification of complexity
ORGANIZING COMMITTEE:
Conf. & PC Co-Chair: Mai Gehrke, LJAD CNRS, France
Conf. & PC Co-Chair: Uli Fahrenberg, Ecole polytechnique, France
Conf. & PC Co-Chair: Michael Winter, Brock University, Canada
Conf. & PC Co-Chair: Luigi Santocanale, LIS, Aix-Marseille University, France
For more information, see https://ramics19.lis-lab.fr/
TABLEAUX 2021
The 30th International Conference on Automated Reasoning with Analytic
Tableaux and Related Methods
Online and Birmingham, UK, September 6-9, 2021
https://tableaux2021.org/
GENERAL INFORMATION
The 30th International Conference on Automated Reasoning with Analytic
Tableaux and Related Methods (TABLEAUX 2021) will be hosted by the
University of Birmingham, UK, 6-9 September 2021. It will primarily be
a virtual conference, due to ongoing conerns about COVID-19. However it
will be possible to attend the conference physically for those who are
able to travel to Birmingham and take advantage of a hybrid format.
TABLEAUX is the main international conference at which research on all
aspects -- theoretical foundations, implementation techniques, systems
development and applications -- of tableaux-based reasoning and related
methods is presented. The first TABLEAUX conference was held in
Lautenbach near Karlsruhe, Germany, in 1992. Since then it has been
organised on an annual basis (sometimes as a part of IJCAR).
TABLEAUX 2021 will be co-located with the 13th International Symposium
on Frontiers of Combining Systems (FroCoS 2021).
SCOPE OF CONFERENCE
Tableaux and other proof based methods offer convenient and flexible
tools for automated reasoning for both classical and non-classical
logics. Areas of application include verification of software and
computer systems, deductive databases, knowledge representation and its
required inference engines, teaching, and system diagnosis.
Topics of interest include but are not limited to:
* tableau methods for classical and non-classical logics (including
first-order, higher-order, modal, temporal, description, hybrid,
intuitionistic, linear, substructural, fuzzy, relevance and non-
monotonic logics) and their proof-theoretic foundations;
* sequent, natural deduction, labelled, nested and deep calculi for
classical and non-classical logics, as tools for proof search and proof
representation;
* related methods (SMT, model elimination, model checking,
connection methods, resolution, BDDs, translation approaches);
* flexible, easily extendable, light-weight methods for theorem
proving; novel types of calculi for theorem proving and verification in
classical and non-classical logics;
* systems, tools, implementations, empirical evaluations and
applications (provers, proof assistants, logical frameworks, model
checkers, etc.);
* implementation techniques (data structures, efficient algorithms,
performance measurement, extensibility, etc.);
* extensions of tableau procedures with conflict-driven learning;
* techniques for proof generation and compact (or humanly readable)
proof representation;
* theoretical and practical aspects of decision procedures;
* applications of automated deduction to mathematics, software
development, verification, deductive and temporal databases, knowledge
representation, ontologies, fault diagnosis or teaching.
We also welcome papers describing applications of tableau procedures to
real-world examples. Such papers should be tailored to the TABLEAUX
community and should focus on the role of reasoning and on logical
aspects of the solution.
INVITED SPEAKERS
TABLEAUX 2021 will host the following the invited speakers:
Michael Benedikt (joint with FroCoS) (University of Oxford, UK). The
Strange Career of Interpolation and Definability.
Orna Kupferman (Hebrew University, Israel). Rational Synthesis.
Revantha Ramanayake (University of Groningen, The Netherlands). The
Barter Trade in Structure and Cuts.
Greg Restall (University of Melbourne, Australia / University of St
Andrews, UK). Comparing Rules for Identity in Sequent Systems and
Natural Deduction.
Renate Schmidt (joint with FroCoS) (University of Manchester, UK).
Forgetting and Subontology Generation for the Medical Ontology SNOMED
CT.
PROGRAM
The program can be found here: https://tableaux2021.org/#program .
REGISTRATION
TABLEAUX and FroCoS will be entirely free-of-charge to attend, but
registration is mandatory to fully engage with the scientific program.
The registration form is here:
https://forms.gle/DRNBgeRKA4Qbcsws7
If you wish to attend physically, you should indicate it on the
registration form. Note that you are able to edit this response in case
of change of circumstances. More information about the conference
format will be updated here.
PROGRAM COMMITTEE
Bahareh Afshari (University of Amsterdam, Netherlands, and University
of Gothenburg, Sweden)
Carlos Areces (Universidad Nacional de Córdoba, Argentina)
Arnon Avron (Tel-Aviv University, Israel)
Nick Bezhanishvili (University of Amsterdam, Netherlands)
Patrick Blackburn (University of Roskilde, Denmark)
Serenella Cerrito (Université Paris-Saclay, Univ Evry, France)
Kaustuv Chaudhuri (Inria, France)
Liron Cohen (Ben-Gurion University, Israel)
Anupam Das (University of Birmingham, UK)
Stéphane Demri (CNRS, France)
Hans de Nivelle (Nazarbayev University, Kazakhstan)
Valeria de Paiva (Topos Institute Berkeley, USA)
Clare Dixon (University of Manchester, UK)
Christian Fermüller (TU Wien, Austria)
Didier Galmiche (Université de Lorraine, France)
Silvio Ghilardi (Università degli Studi di Milano, Italy)
Rajeev Goré (Australian National University, Australia)
Andrzej Indrzejczak (University of Łódź, Poland)
Hidenori Kurokawa (Kanazawa University, Japan)
Stepan Kuznetsov (Russian Academy of Sciences, Russia)
Björn Lellmann (SBA Research, Austria)
Stéphane Graham-Lengrand (SRI International, USA)
George Metcalfe (University of Bern, Switzerland)
Neil Murray (University At Albany, USA)
Cláudia Nalon (Universidade de Brasília, Brazil)
Sara Negri (University of Genoa, Italy)
Nicola Olivetti (Aix-Marseille University, France)
Eugenio Orlandelli (University of Bologna, Italy)
Jens Otten (University of Oslo, Norway)
Alessandra Palmigiano (Vrije Universiteit Amsterdam, Netherlands)
Dirk Pattinson (Australian National University, Australia)
Frank Pfenning (Carnegie Mellon University, USA)
Elaine Pimentel (Federal University of Rio Grande do Norte, Brazil)
Andrei Popescu (University of Sheffield, UK)
Gian Luca Pozzato (University of Turin, Italy)
Giselle Reis (Carnegie Mellon University, Qatar)
Reuben Rowe (Royal Holloway, UK)
José Espírito Santo (University of Minho, Portugal)
Lutz Straßburger (Inria, France)
Josef Urban (Czech Technical University in Prague, Czech Republic)
PC CHAIRS
Anupam Das (University of Birmingham, UK)
Sara Negri (University of Genoa, Italy)
von Titolo, Laura (LARC-D320)[NATIONAL INSTITUTE OF AEROSPACE] via fm-announcements
Certified Programs and Proofs (CPP) is an international conference on
practical and theoretical topics in all areas that consider formal
verification and certification as an essential paradigm for their
work. CPP spans areas of computer science, mathematics, logic, and
education.
CPP 2022 (https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fpopl22.si…) will be held on
17-18 January 2022 and will be co-located with POPL 2022 in
Philadelphia, Pennsylvania, United States. CPP 2022 is sponsored by
ACM SIGPLAN, in cooperation with ACM SIGLOG.
CPP 2022 will welcome contributions from all members of the community.
The CPP 2022 organizers will strive to enable both in-person and
remote participation, in cooperation with the POPL 2022 organizers.
NEWS
If the authors of a CPP 2022 accepted paper will be unable or
unwilling to travel to the conference, the organizers can confirm that
this will not affect the paper’s publication in the proceedings, and
the authors will be able to upload recorded talks that will be made
publicly available.
IMPORTANT DATES
* Abstract Submission Deadline: 16 September 2021 at 23:59 AoE (UTC-12h)
* Paper Submission Deadline: 22 September 2021 at 23:59 AoE (UTC-12h)
* Notification (tentative): 22 November 2021
* Camera Ready Deadline (tentative): 12 December 2021
* Conference: 17-18 January 2022
Deadlines expire at the end of the day, anywhere on earth. Abstract
and submission deadlines are strict and there will be no extensions.
DISTINGUISHED PAPER AWARDS
Around 10% of the accepted papers at CPP 2022 will be designated as
Distinguished Papers. This award highlights papers that the CPP
program committee thinks should be read by a broad audience due to
their relevance, originality, significance and clarity.
TOPICS OF INTEREST
We welcome submissions in research areas related to formal
certification of programs and proofs. The following is a
non-exhaustive list of topics of interest to CPP:
* certified or certifying programming, compilation, linking, OS
kernels, runtime systems, security monitors, and hardware;
* certified mathematical libraries and mathematical theorems;
* proof assistants (e.g, ACL2, Agda, Coq, Dafny, F*, HOL4, HOL Light,
Idris, Isabelle, Lean, Mizar, Nuprl, PVS, etc);
* new languages and tools for certified programming;
* program analysis, program verification, and program synthesis;
* program logics, type systems, and semantics for certified code;
* logics for certifying concurrent and distributed systems;
* mechanized metatheory, formalized programming language semantics,
and logical frameworks;
* higher-order logics, dependent type theory, proof theory, logical
systems, separation logics, and logics for security;
* verification of correctness and security properties;
* formally verified blockchains and smart contracts;
* 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;
* formal models of computation;
* mechanized (un)decidability and computational complexity proofs;
* formally certified methods for induction and coinduction;
* integration of interactive and automated provers;
* logical foundations of proof assistants;
* applications of AI and machine learning to formal certification;
* user interfaces for proof assistants and theorem provers;
* teaching mathematics and computer science with proof assistants.
SUBMISSION GUIDELINES
Prior to the paper submission deadline, the authors should upload
their anonymized paper in PDF format through the HotCRP system at
https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fcpp2022.h…
The submissions must be written in English and provide sufficient
detail to allow the program committee to assess the merits of the
contribution. They must be formatted following the ACM SIGPLAN
Proceedings format using the acmart style with the sigplan option,
which provides a two-column style, using 10 point font for the main
text, and a header for double blind review submission, i.e.,
\documentclass[sigplan,10pt,anonymous,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
The submitted papers should not exceed 12 pages, including tables and
figures, but excluding bibliography and clearly marked appendices. The
papers should be self-contained without the appendices. Shorter papers
are welcome and will be given equal consideration. Submissions not
conforming to the requirements concerning format and maximum length
may be rejected without further consideration.
CPP 2022 will employ a lightweight double-blind reviewing process. To
facilitate this, the submissions must adhere to two rules:
(1) author names and institutions must be omitted, and
(2) references to authors’ own related work should be in the third
person (e.g., not "We build on our previous work ..." but rather "We
build on the work of ...").
The purpose of this process is to help the PC and external reviewers
come to an initial judgment about the paper without bias, not to make
it impossible for them to discover the authors if they were to try.
Nothing should be done in the name of anonymity that weakens the
submission or makes the job of reviewing it more difficult. In
particular, important background references should not be omitted or
anonymized. In addition, authors are free to disseminate their ideas
or draft versions of their papers as usual. For example, authors may
post drafts of their papers on the web or give talks on their research
ideas. POPL has answers to frequently asked questions addressing many
common concerns: https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fpopl20.si…
We strongly encourage the authors to provide any supplementary
material that supports the claims made in the paper, such as proof
scripts or experimental data. This material must be uploaded at
submission time, as an archive, not via a URL. Two forms of
supplementary material may be submitted:
(1) Anonymous supplementary material is made available to the
reviewers before they submit their first-draft reviews.
(2) Non-anonymous supplementary material is made available to the
reviewers after they have submitted their first-draft reviews and have
learned the identity of the authors.
Please use anonymous supplementary material whenever possible, so that
it can be taken into account from the beginning of the reviewing
process.
The submitted papers must adhere to the SIGPLAN Republication Policy
(https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.sigpl…) and the
ACM Policy on Plagiarism
(https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.acm.o…);reserved=0).
Concurrent submissions to other conferences, journals, workshops with
proceedings, or similar forums of publication are not allowed. The PC
chairs should be informed of closely related work submitted to a
conference or journal in advance of submission. One author of each
accepted paper is expected to present it at the (possibly virtual)
conference.
PUBLICATION, COPYRIGHT AND OPEN ACCESS
The CPP 2022 proceedings will be published by the ACM, and authors of
accepted papers will be required to choose one of the following
publication options:
(1) Author retains copyright of the work and grants ACM a
non-exclusive permission-to-publish license and, optionally, licenses
the work under a Creative Commons license.
(2) Author retains copyright of the work and grants ACM an exclusive
permission-to-publish license.
(3) Author transfers copyright of the work to ACM.
For authors who can afford it, we recommend option (1), which will
make the paper Gold Open Access, and also encourage such authors to
license their work under the CC-BY license. ACM will charge you an
article processing fee for this option (currently, US$700), which you
have to pay directly with the ACM.
For everyone else, we recommend option (2), which is free and allows
you to achieve Green Open Access, by uploading a preprint of your
paper to a repository that guarantees permanent archival such as arXiv
or HAL. This is anyway a good idea for timely dissemination even if
you chose option 1. Ensuring timely dissemination is particularly
important for this edition, since, because of the very tight schedule,
the official proceedings might not be available in time for CPP.
The official CPP 2022 proceedings will also be available via SIGPLAN
OpenTOC (https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.sigpl…);reserved=0).
For ACM’s take on this, see their Copyright Policy
(https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.acm.o…) and Author
Rights (https://gcc02.safelinks.protection.outlook.com/?url=https%3A%2F%2Fauthors.a…);reserved=0).
PROGRAM COMMITTEE
Andrei Popescu, University of Sheffield, United Kingdom (co-chair)
Steve Zdancewic, University of Pennsylvania, United States (co-chair)
Mohammad Abdulaziz, TU München, Germany
Mauricio Ayala-Rincón, Universidade de Brasília, Brazil
Andrej Bauer, University of Ljubljana, Slovenia
Thomas Bauereiss, University of Cambridge, United Kingdom
Yves Bertot, Inria and Université Cote d'Azur, France
Lars Birkedal, Aarhus University, Denmark
Sylvie Boldo, Inria and Université Paris-Saclay, France
Qinxiang Cao, Shanghai Jiao Tong University, China
Évelyne Contejean, Laboratoire Méthodes Formelles, CNRS, France
Benjamin Delaware, Purdue University, United States
Simon Foster, University of York, United Kingdom
Alwyn Goodloe, NASA Langley Research Center, United States
Armaël Guéneau, Aarhus University, Denmark
John Harrison, Amazon Web Services, United States
Joe Hendrix, Galois, Inc, United States
Aquinas Hobor, National University of Singapore, Singapore
Ralf Jung, MPI-SWS, Germany
Cezary Kaliszyk, University of Innsbruck, Austria
Jeehoon Kang, KAIST, South Korea
Hongjin Liang, Nanjing University, China
Gregory Malecha, BedRock Systems, Inc, United States
Anders Mörtberg, Stockholm University, Sweden
Toby Murray, University of Melbourne, Australia
Zoe Paraskevopoulou , Northeastern University, United States
Brigitte Pientka, McGill University, Canada
Aseem Rastogi, Microsoft Research, India
Bas Spitters, Aarhus University, Denmark
Kathrin Stark, Princeton University, United States
Hira Taqdees Syeda, Chalmers University of Technology, Sweden
Joseph Tassarotti, Boston College, United States
Laura Titolo, NIA/NASA LaRC, United States
Sophie Tourret, Inria, France
Dmitriy Traytel, University of Copenhagen, Denmark
Floris van Doorn, Paris-Saclay University, France
Freek Verbeek, Open University of The Netherlands, Netherlands
Freek Wiedijk, Radboud Universiteit Nijmegen, Netherlands
ORGANIZERS
Lennart Beringer, Princeton University, United States (conference co-chair)
Robbert Krebbers, Radboud University, Netherlands (conference co-chair)
Andrei Popescu, University of Sheffield, United Kingdom (PC co-chair)
Steve Zdancewic, University of Pennsylvania, United States (PC co-chair)
CONTACT
For any questions please contact the two PC chairs:
Andrei Popescu <mailto:a.popescu@sheffield.ac.uk>
Steve Zdancewic <mailto:stevez@seas.upenn.edu>
---
To opt-out from this mailing list, send an email to
fm-announcements-request(a)lists.nasa.gov
with the word 'unsubscribe' as subject or in the body. You can also make the request by contacting
fm-announcements-owner(a)lists.nasa.gov
Certified Programs and Proofs (CPP) is an international conference on
practical and theoretical topics in all areas that consider formal
verification and certification as an essential paradigm for their
work. CPP spans areas of computer science, mathematics, logic, and
education.
CPP 2022 (https://popl22.sigplan.org/home/CPP-2022) will be held on
17-18 January 2022 and will be co-located with POPL 2022 in
Philadelphia, Pennsylvania, United States. CPP 2022 is sponsored by
ACM SIGPLAN, in cooperation with ACM SIGLOG.
CPP 2022 will welcome contributions from all members of the community.
The CPP 2022 organizers will strive to enable both in-person and
remote participation, in cooperation with the POPL 2022 organizers.
NEWS
If the authors of a CPP 2022 accepted paper will be unable or
unwilling to travel to the conference, the organizers can confirm that
this will not affect the paper’s publication in the proceedings, and
the authors will be able to upload recorded talks that will be made
publicly available.
IMPORTANT DATES
* Abstract Submission Deadline: 16 September 2021 at 23:59 AoE (UTC-12h)
* Paper Submission Deadline: 22 September 2021 at 23:59 AoE (UTC-12h)
* Notification (tentative): 22 November 2021
* Camera Ready Deadline (tentative): 12 December 2021
* Conference: 17-18 January 2022
Deadlines expire at the end of the day, anywhere on earth. Abstract
and submission deadlines are strict and there will be no extensions.
DISTINGUISHED PAPER AWARDS
Around 10% of the accepted papers at CPP 2022 will be designated as
Distinguished Papers. This award highlights papers that the CPP
program committee thinks should be read by a broad audience due to
their relevance, originality, significance and clarity.
TOPICS OF INTEREST
We welcome submissions in research areas related to formal
certification of programs and proofs. The following is a
non-exhaustive list of topics of interest to CPP:
* certified or certifying programming, compilation, linking, OS
kernels, runtime systems, security monitors, and hardware;
* certified mathematical libraries and mathematical theorems;
* proof assistants (e.g, ACL2, Agda, Coq, Dafny, F*, HOL4, HOL Light,
Idris, Isabelle, Lean, Mizar, Nuprl, PVS, etc);
* new languages and tools for certified programming;
* program analysis, program verification, and program synthesis;
* program logics, type systems, and semantics for certified code;
* logics for certifying concurrent and distributed systems;
* mechanized metatheory, formalized programming language semantics,
and logical frameworks;
* higher-order logics, dependent type theory, proof theory, logical
systems, separation logics, and logics for security;
* verification of correctness and security properties;
* formally verified blockchains and smart contracts;
* 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;
* formal models of computation;
* mechanized (un)decidability and computational complexity proofs;
* formally certified methods for induction and coinduction;
* integration of interactive and automated provers;
* logical foundations of proof assistants;
* applications of AI and machine learning to formal certification;
* user interfaces for proof assistants and theorem provers;
* teaching mathematics and computer science with proof assistants.
SUBMISSION GUIDELINES
Prior to the paper submission deadline, the authors should upload
their anonymized paper in PDF format through the HotCRP system at
https://cpp2022.hotcrp.com
The submissions must be written in English and provide sufficient
detail to allow the program committee to assess the merits of the
contribution. They must be formatted following the ACM SIGPLAN
Proceedings format using the acmart style with the sigplan option,
which provides a two-column style, using 10 point font for the main
text, and a header for double blind review submission, i.e.,
\documentclass[sigplan,10pt,anonymous,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
The submitted papers should not exceed 12 pages, including tables and
figures, but excluding bibliography and clearly marked appendices. The
papers should be self-contained without the appendices. Shorter papers
are welcome and will be given equal consideration. Submissions not
conforming to the requirements concerning format and maximum length
may be rejected without further consideration.
CPP 2022 will employ a lightweight double-blind reviewing process. To
facilitate this, the submissions must adhere to two rules:
(1) author names and institutions must be omitted, and
(2) references to authors’ own related work should be in the third
person (e.g., not "We build on our previous work ..." but rather "We
build on the work of ...").
The purpose of this process is to help the PC and external reviewers
come to an initial judgment about the paper without bias, not to make
it impossible for them to discover the authors if they were to try.
Nothing should be done in the name of anonymity that weakens the
submission or makes the job of reviewing it more difficult. In
particular, important background references should not be omitted or
anonymized. In addition, authors are free to disseminate their ideas
or draft versions of their papers as usual. For example, authors may
post drafts of their papers on the web or give talks on their research
ideas. POPL has answers to frequently asked questions addressing many
common concerns:
https://popl20.sigplan.org/track/POPL-2020-Research-Papers#Submission-and-R…
We strongly encourage the authors to provide any supplementary
material that supports the claims made in the paper, such as proof
scripts or experimental data. This material must be uploaded at
submission time, as an archive, not via a URL. Two forms of
supplementary material may be submitted:
(1) Anonymous supplementary material is made available to the
reviewers before they submit their first-draft reviews.
(2) Non-anonymous supplementary material is made available to the
reviewers after they have submitted their first-draft reviews and have
learned the identity of the authors.
Please use anonymous supplementary material whenever possible, so that
it can be taken into account from the beginning of the reviewing
process.
The submitted papers must adhere to the SIGPLAN Republication Policy
(https://www.sigplan.org/Resources/Policies/Republication/) and the
ACM Policy on Plagiarism
(https://www.acm.org/publications/policies/plagiarism). Concurrent
submissions to other conferences, journals, workshops with
proceedings, or similar forums of publication are not allowed. The PC
chairs should be informed of closely related work submitted to a
conference or journal in advance of submission. One author of each
accepted paper is expected to present it at the (possibly virtual)
conference.
PUBLICATION, COPYRIGHT AND OPEN ACCESS
The CPP 2022 proceedings will be published by the ACM, and authors of
accepted papers will be required to choose one of the following
publication options:
(1) Author retains copyright of the work and grants ACM a
non-exclusive permission-to-publish license and, optionally, licenses
the work under a Creative Commons license.
(2) Author retains copyright of the work and grants ACM an exclusive
permission-to-publish license.
(3) Author transfers copyright of the work to ACM.
For authors who can afford it, we recommend option (1), which will
make the paper Gold Open Access, and also encourage such authors to
license their work under the CC-BY license. ACM will charge you an
article processing fee for this option (currently, US$700), which you
have to pay directly with the ACM.
For everyone else, we recommend option (2), which is free and allows
you to achieve Green Open Access, by uploading a preprint of your
paper to a repository that guarantees permanent archival such as arXiv
or HAL. This is anyway a good idea for timely dissemination even if
you chose option 1. Ensuring timely dissemination is particularly
important for this edition, since, because of the very tight schedule,
the official proceedings might not be available in time for CPP.
The official CPP 2022 proceedings will also be available via SIGPLAN
OpenTOC (http://www.sigplan.org/OpenTOC/#cpp).
For ACM’s take on this, see their Copyright Policy
(http://www.acm.org/publications/policies/copyright-policy) and Author
Rights (http://authors.acm.org/main.html).
PROGRAM COMMITTEE
Andrei Popescu, University of Sheffield, United Kingdom (co-chair)
Steve Zdancewic, University of Pennsylvania, United States (co-chair)
Mohammad Abdulaziz, TU München, Germany
Mauricio Ayala-Rincón, Universidade de Brasília, Brazil
Andrej Bauer, University of Ljubljana, Slovenia
Thomas Bauereiss, University of Cambridge, United Kingdom
Yves Bertot, Inria and Université Cote d'Azur, France
Lars Birkedal, Aarhus University, Denmark
Sylvie Boldo, Inria and Université Paris-Saclay, France
Qinxiang Cao, Shanghai Jiao Tong University, China
Évelyne Contejean, Laboratoire Méthodes Formelles, CNRS, France
Benjamin Delaware, Purdue University, United States
Simon Foster, University of York, United Kingdom
Alwyn Goodloe, NASA Langley Research Center, United States
Armaël Guéneau, Aarhus University, Denmark
John Harrison, Amazon Web Services, United States
Joe Hendrix, Galois, Inc, United States
Aquinas Hobor, National University of Singapore, Singapore
Ralf Jung, MPI-SWS, Germany
Cezary Kaliszyk, University of Innsbruck, Austria
Jeehoon Kang, KAIST, South Korea
Hongjin Liang, Nanjing University, China
Gregory Malecha, BedRock Systems, Inc, United States
Anders Mörtberg, Stockholm University, Sweden
Toby Murray, University of Melbourne, Australia
Zoe Paraskevopoulou , Northeastern University, United States
Brigitte Pientka, McGill University, Canada
Aseem Rastogi, Microsoft Research, India
Bas Spitters, Aarhus University, Denmark
Kathrin Stark, Princeton University, United States
Hira Taqdees Syeda, Chalmers University of Technology, Sweden
Joseph Tassarotti, Boston College, United States
Laura Titolo, NIA/NASA LaRC, United States
Sophie Tourret, Inria, France
Dmitriy Traytel, University of Copenhagen, Denmark
Floris van Doorn, Paris-Saclay University, France
Freek Verbeek, Open University of The Netherlands, Netherlands
Freek Wiedijk, Radboud Universiteit Nijmegen, Netherlands
ORGANIZERS
Lennart Beringer, Princeton University, United States (conference co-chair)
Robbert Krebbers, Radboud University, Netherlands (conference co-chair)
Andrei Popescu, University of Sheffield, United Kingdom (PC co-chair)
Steve Zdancewic, University of Pennsylvania, United States (PC co-chair)
CONTACT
For any questions please contact the two PC chairs:
Andrei Popescu <a.popescu(a)sheffield.ac.uk>
Steve Zdancewic <stevez(a)seas.upenn.edu>