----------------------------------------------------------------------
**
** **** CALL FOR SUBMISSIONS ****
**
** HOR 2023 - 11th International Workshop on Higher-Order Rewriting
** 4 July 2023
** Rome, Italy
**
** https://hor2023.github.io/
----------------------------------------------------------------------
**
** HOR 2023 is affiliated with FSCD 2023
** https://easyconferences.eu/fscd2023/
**
----------------------------------------------------------------------
* OVERVIEW
HOR is a forum to present work concerning all aspects of higher-order
rewriting.
HOR aims to provide an informal and friendly setting to discuss recent
work and work in progress concerning higher-order rewriting, broadly
construed. This includes rewriting systems that have functional
variables or bound variables, the lambda-calculus and combinatory
logic being paradigmatic examples.
* TOPICS
The following is a non-exhaustive list of topics for the workshop:
- Applications: proof checking, theorem proving, generic
programming, declarative programming, program transformation,
automated termination/confluence/equivalence analysis tools.
- Foundations: pattern matching, unification, strategies, narrowing,
termination, syntactic properties, type theory, complexity of
derivations.
- Frameworks: term rewriting, conditional rewriting, graph
rewriting, net rewriting, comparisons of different frameworks.
- Implementation: explicit substitution, rewriting tools,
compilation techniques.
- Semantics: semantics of higher-order rewriting, categorical
rewriting, higher-order abstract syntax, games and rewriting.
----------------------------------------------------------------------
** SUBMISSION GUIDELINES
----------------------------------------------------------------------
To give a presentation at the workshop, please submit an extended
abstract (between 2 to 5 pages) via Easychair:
https://easychair.org/conferences/?conf=hor2023
Please use LaTeX and the Easychair style to prepare your submission:
https://easychair.org/publications/easychair.zip
HOR is a platform for discussing open questions, ongoing research,
and new perspectives, as well as new results. Extended abstracts
describing work in progress, preliminary results, research projects,
or problems in higher-order rewriting are very welcome. Specifically,
short versions of recently published papers are welcome, and
submission to HOR does not preclude formal publication at other
venues.
The workshop has informal electronic proceedings that will be made
available on the workshop website.
----------------------------------------------------------------------
** IMPORTANT DATES
----------------------------------------------------------------------
* Submission deadline: 2 May 2023
* Notification: 29 May 2023
* Final version: 12 June 2023
----------------------------------------------------------------------
** COMMITTEES
----------------------------------------------------------------------
** PROGRAM COMMITTEE
* Takahito Aoto - Niigata University, Japan
* Maribel Fernández - King's College London, United Kingdom
* Carsten Fuhs (Chair) - Birkbeck, University of London, United Kingdom
* Delia Kesner - Université Paris 7, France
* Cynthia Kop - Radboud Universiteit Nijmegen, The Netherlands
* Damiano Mazza - Université Paris 13, France
----------------------------------------------------------------------
** STEERING COMMITTEE
* Delia Kesner, Université Paris 7, France
* Femke van Raamsdonk, Vrije Universiteit, The Netherlands
----------------------------------------------------------------------
** CONTACT
----------------------------------------------------------------------
All questions about submissions should be emailed to the PC chair
Carsten Fuhs (hor2023 at easychair.org)
(Apologies for multiple copies of this announcement. Please circulate.)
---------------
Call for Location for FSCD 2025
The FSCD conference covers all aspects of Formal Structures for
Computation and Deduction from theoretical foundations to
applications. The annual FSCD conference comprises the main
conference and a considerable number of affiliated workshops
(expectedly, more than ten).
We invite proposals for locations to host the 10th FSCD International
Conference to be held during the summer of 2025. The deadline for proposals is
*** 27th May 2023 ***
Proposals should be sent to the FSCD Steering Committee Chair (see
contact information below). We encourage proposers to register their
intention informally as soon as possible.
Previous (and upcoming) FSCD meetings include:
FSCD 2016 in Porto (Portugal);
FSCD 2017 in Oxford (UK) co-located with ICFP 2017;
FSCD 2018 in Oxford (UK) as part of FLoC 2018;
FSCD 2019 in Dortmund (Germany);
FSCD 2020 in Paris (France) co-located with IJCAR 2020;
FSCD 2021 in Buenos Aires (Argentina);
FSCD 2022 in Haifa (Israel) as part of FLOC2022;
FSCD 2023 in Rome (Italy) co-located with CADE 2023;
FSCD 2024 in Tallinn (Estonia).
Selected proposals are to be presented at the business meeting of FSCD
2023 taking place in Rome in July 2023. The final decision about
hosting and organising of FSCD 2025 will be taken by the SC after an
advisory vote of the members of the community in attendance at the
business meeting.
Proposals should address the following points:
* FSCD Conference Chair (complete name and current position), host
institution, FSCD Local Committee (complete names and current
positions), availability of student-volunteers.
* National, regional, and local government and industry support, both
organizational and financial.
* Accessibility to the location (i.e., transportation) and
attractiveness of the proposed site. Accessibility can include both
information about local transportation and travel information to the
location (flight and/or train connections), as well as estimated
costs.
* Proposed dates, including allowing 2-3 days before and/or after the
main conference for affiliated workshops. (Please also take into
consideration holidays or local events during the period).
* Estimated costs of registration for the conference and workshops,
both for regular and student participants.
* Conference and exhibit facilities for the anticipated number of
registrants (including all workshop participants, typically around 200).
For example:
= number, capacity and audiovisual equipment of meeting rooms;
= a large plenary session room that can hold all the registrants;
= enough rooms for parallel session workshops/tutorials in the two
days before and the two days after the main conference;
= internet connectivity and workstations for demos/competitions;
= catering services;
= presence of professional staff.
* Support for hybrid attendance to the conference.
* Residence accommodations and food services in a range of price
categories and close to the conference venue, for example, number
and cost range of hotels, and availability and cost of dormitory
rooms (e.g., at local universities) and kind of services they offer.
* Other relevant information, which can include information about
leisure activities and attractiveness of the location (e.g.,
cultural and historical aspects, touristic activities, etc...).
Contact information:
Herman Geuvers
herman(a)cs.ru.nl
FSCD SC Chair
==============================================================================
Updated information on: EXTENDED DEADLINE for submission
==============================================================================
LAST CALL FOR PAPERS
Eighth International Conference on
Formal Structures for Computation and Deduction (FSCD 2023)
July 3-6, 2023, Rome, Italy
https://easyconferences.eu/fscd2023/
In-cooperation with ACM SIGLOG and SIGPLAN
IMPORTANT DATES
---------------
All deadlines are midnight anywhere-on-earth (AoE); late submissions will not be considered.
Abstract: EXTENDED to February 4, 2023
Submission: EXTENDED to February 9, 2023
Rebuttal: March 24-28, 2023 (not changed)
Notification: April 13, 2023 (not changed)
Final version: April 27, 2023 (not changed)
CO-LOCATION AND AFFILIATED WORKSHOPS
------------------------------------
FSCD 2023 will be co-located with CADE-29. The following workshops are affiliated with FSCD and CADE in 2023:
- WIL: 7th Workshop Women in Logic (July 1, 2023)
- WPTE: 10th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (July 1, 2023)
- TLLA: 7th International Workshop on Trends in Linear Logic and Applications (July 1-2, 2023)
- LSFA: 8th Logical and Semantic Frameworks with Applications (July 1-2, 2023)
- DCM: 13th International Workshop on Developments in Computational Models (July 2, 2023)
- LFMTP: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (July 2, 2023)
- UNIF: 37th International Workshop on Unification (July 2, 2023)
- CASC: The CADE ATP System Competition (July 3, 2023)
- HOR: 11th International Workshop on Higher-Order Rewriting (July 4, 2023)
- SMT: 21st International Workshop on Satisfiability Modulo Theories (July 4-6, 2023)
- ADeMaL: Automated Deduction for Machine Learning (July 5, 2023)
- ThEdu: Theorem proving components for Educational software (July 5, 2023)
- Vampire: 7th Vampire Workshop (July 5, 2023)
- IFIP WG 1.6: Annual Meeting of IFIP Working Group 1.6 on Rewriting (July 5, 2023)
OVERVIEW
--------
FSCD (https://fscd-conference.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 logic, models of computation, semantics and verification in new challenging areas.
The suggested, but not exclusive, list of topics for submission is:
1. Calculi:
- Rewriting systems (string, term, higher-order, graph, conditional, modulo, infinitary, etc.);
- Lambda calculus;
- Logics (first-order, higher-order, equational, modal, linear, classical, constructive, etc.);
- Proof theory (natural deduction, sequent calculus, proof nets, etc.);
- Type theory and logical frameworks;
- Homotopy type theory;
- Quantum calculi.
2. Methods in Computation and Deduction:
- Type systems (polymorphism, dependent, recursive, intersection, session, etc.);
- Induction, coinduction;
- Matching, unification, completion, orderings;
- Strategies (normalization, completeness, etc.);
- Tree automata;
- Model building and model checking;
- Proof search and theorem proving;
- Constraint solving and decision procedures.
3. Semantics:
- Operational semantics and abstract machines;
- Game Semantics and applications;
- Domain theory and categorical models;
- Quantitative models (timing, probabilities, etc.);
- Quantum computation and emerging models in computation.
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;
- Proof assistants and interactive theorem provers;
- Applications in industry;
- Applications of formal systems in other sciences;
- Applications of formal systems in education.
6. Formal Systems for Semantics and Verification in new challenging areas:
- Certification;
- Security;
- Blockchain protocols;
- Data bases;
- Deep learning and machine learning algorithms;
- Planning.
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.
SPECIAL ISSUE
-------------
Authors of selected papers will be invited to submit an extended version to a special issue of Logical Methods in Computer Science, or to TheoretiCS.
SUBMISSION GUIDELINES
---------------------
The submission site is:
https://easychair.org/conferences/?conf=fscd2023
Submissions must be formatted using the LIPIcs style files (https://submission.dagstuhl.de/series/details/5#author) and submitted via EasyChair.
Submissions can be made in two categories. Regular research papers are limited to 15 pages, excluding references and appendices. They must present original research which is unpublished and not submitted elsewhere. System descriptions are limited to 15 pages, excluding references. Shorter papers are welcome and will be given equal consideration.
A system description must present new software tools, or significantly new versions of such tools, in which FSCD topics play an important role. An archive of the code with instructions on how to install and run the tool must be submitted. In addition, a webpage where the system can be experimented with should be provided.
One author of each accepted paper is expected to register and present the work in person at the conference. Alternatively to in-person presentation, also online presentation is possible, but in-person registration by at least one author will still be required.
BEST PAPER AWARD BY JUNIOR RESEARCHERS
--------------------------------------
The program committee will select a paper in which at least one author is a junior researcher, i.e. either a student or whose PhD award date is less than three years from the first day of the meeting. When submitting the paper, other authors should declare to the PC Chairs that at least 50% of contribution is made by the junior researcher(s).
PROGRAM COMMITTEE CHAIRS
------------------------
Marco Gaboardi, Boston University
Femke van Raamsdonk, Vrije Universiteit Amsterdam
Email: fscd2023 at easychair.org
PROGRAM COMMITTEE
-----------------
Martin Avanzini, INRIA
Patrick Bahr, ITU Copenhagen
Pablo Barenbaum, University of Quilmes (CONICET) & ICC
Filippo Bonchi, University of Pisa
Sabine Broda, University of Porto
Valeria De Paiva, Topos Institute
Andrej Dudenhefner, TU Dortmund
Santiago Escobar, Universitat Politècnica de València
Claudia Faggian, University of Paris (IRIF)
Frank (Peng) Fu, Dalhousie University
Silvio Ghilardi, University of Milano
Clemens Grabmayer, GSSI or Gran Sasso Science Institute
Nao Hirokawa, JAIST
Mirai Ikebuchi, National Institute of Informatics
Ambrus Kaposi, Eotvos Lorand University
Ian Mackie, University of Sussex
Radu Mardare, University of Strathclyde
Aart Middeldorp, University of Innsbruck
Anders Mortberg, University of Stockholm
Daniele Nantes-Sobrinho, Imperial College London / University of Brasília
Vincent van Oostrom, Independent researcher
Grigore Rosu, University of Illinois Urbana-Champaign
Luca Roversi, University of Torino
Aleksy Schubert, University of Warsaw
Jakob G. Simonsen, University of Copenhagen
Alwen Tiu, Australian National University
Valeria Vignudelli, CNRS/ENS Lyon
Johannes Waldmann, HTWK Leipzig
Sarah Winkler, University of Bolzano
CONFERENCE CHAIR
----------------
Daniele Gorla, University of Rome - Sapienza
WORKSHOP CHAIR
--------------
Ivano Salvo, University of Rome - Sapienza
STEERING COMMITTEE WORKSHOP CHAIR
--------------------------------
Cynthia Kop, Radboud University Nijmegen
PUBLICITY CHAIR
---------------
Carsten Fuhs, Birkbeck, University of London
FSCD STEERING COMMITTEE
-----------------------
Zena Ariola, University of Oregon
Alejandro Díaz-Caro, Quilmes University & ICC/CONICET
Amy Felty, University of Ottawa
Carsten Fuhs, Birkbeck, University of London
Herman Geuvers (Chair), Radboud University Nijmegen
Silvia Ghilezan, University of Novi Sad
Jürgen Giesl, RWTH Aachen University
Stefano Guerrini, Université de Paris 13
Delia Kesner, Université de Paris Diderot
Naoki Kobayashi, University of Tokyo
Cynthia Kop, Radboud University Nijmegen
Luigi Liquori, Inria
Daniele Nantes, Imperial College London / University of Brasília
==============================================================================
Updated information on: co-location, affiliated workshops, hybrid presentation
==============================================================================
CALL FOR PAPERS
Eighth International Conference on
Formal Structures for Computation and Deduction (FSCD 2023)
July 3-6, 2023, Rome, Italy
https://easyconferences.eu/fscd2023/
In-cooperation with ACM SIGLOG and SIGPLAN
IMPORTANT DATES
---------------
All deadlines are midnight anywhere-on-earth (AoE); late submissions will not be considered.
Abstract: January 30, 2023
Submission: February 3, 2023
Rebuttal: March 24-28, 2023
Notification: April 13, 2023
Final version: April 27, 2023
CO-LOCATION AND AFFILIATED WORKSHOPS
------------------------------------
FSCD 2023 will be co-located with CADE-29. The following workshops are affiliated with FSCD and CADE in 2023:
- WIL: 7th Workshop Women in Logic (July 1, 2023)
- WPTE: 10th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (July 1, 2023)
- TLLA: 7th International Workshop on Trends in Linear Logic and Applications (July 1-2, 2023)
- LSFA: 8th Logical and Semantic Frameworks with Applications (July 1-2, 2023)
- DCM: 13th International Workshop on Developments in Computational Models (July 2, 2023)
- LFMTP: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (July 2, 2023)
- UNIF: 37th International Workshop on Unification (July 2, 2023)
- CASC: The CADE ATP System Competition (July 3, 2023)
- HOR: 11th International Workshop on Higher-Order Rewriting (July 4, 2023)
- SMT: 21st International Workshop on Satisfiability Modulo Theories (July 4-6, 2023)
- ADeMaL: Automated Deduction for Machine Learning (July 5, 2023)
- ThEdu: Theorem proving components for Educational software (July 5, 2023)
- Vampire: 7th Vampire Workshop (July 5, 2023)
- IFIP WG 1.6: Annual Meeting of IFIP Working Group 1.6 on Rewriting (July 5, 2023)
OVERVIEW
--------
FSCD (https://fscd-conference.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 logic, models of computation, semantics and verification in new challenging areas.
The suggested, but not exclusive, list of topics for submission is:
1. Calculi:
- Rewriting systems (string, term, higher-order, graph, conditional, modulo, infinitary, etc.);
- Lambda calculus;
- Logics (first-order, higher-order, equational, modal, linear, classical, constructive, etc.);
- Proof theory (natural deduction, sequent calculus, proof nets, etc.);
- Type theory and logical frameworks;
- Homotopy type theory;
- Quantum calculi.
2. Methods in Computation and Deduction:
- Type systems (polymorphism, dependent, recursive, intersection, session, etc.);
- Induction, coinduction;
- Matching, unification, completion, orderings;
- Strategies (normalization, completeness, etc.);
- Tree automata;
- Model building and model checking;
- Proof search and theorem proving;
- Constraint solving and decision procedures.
3. Semantics:
- Operational semantics and abstract machines;
- Game Semantics and applications;
- Domain theory and categorical models;
- Quantitative models (timing, probabilities, etc.);
- Quantum computation and emerging models in computation.
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;
- Proof assistants and interactive theorem provers;
- Applications in industry;
- Applications of formal systems in other sciences;
- Applications of formal systems in education.
6. Formal Systems for Semantics and Verification in new challenging areas:
- Certification;
- Security;
- Blockchain protocols;
- Data bases;
- Deep learning and machine learning algorithms;
- Planning.
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.
SPECIAL ISSUE
-------------
Authors of selected papers will be invited to submit an extended version to a special issue of Logical Methods in Computer Science, or to TheoretiCS.
SUBMISSION GUIDELINES
---------------------
The submission site is:
https://easychair.org/conferences/?conf=fscd2023
Submissions must be formatted using the LIPIcs style files (https://submission.dagstuhl.de/series/details/5#author) and submitted via EasyChair.
Submissions can be made in two categories. Regular research papers are limited to 15 pages, excluding references and appendices. They must present original research which is unpublished and not submitted elsewhere. System descriptions are limited to 15 pages, excluding references. Shorter papers are welcome and will be given equal consideration.
A system description must present new software tools, or significantly new versions of such tools, in which FSCD topics play an important role. An archive of the code with instructions on how to install and run the tool must be submitted. In addition, a webpage where the system can be experimented with should be provided.
One author of each accepted paper is expected to register and present the work in person at the conference. Alternatively to in-person presentation, also online presentation is possible, but in-person registration by at least one author will still be required.
BEST PAPER AWARD BY JUNIOR RESEARCHERS
--------------------------------------
The program committee will select a paper in which at least one author is a junior researcher, i.e. either a student or whose PhD award date is less than three years from the first day of the meeting. When submitting the paper, other authors should declare to the PC Chairs that at least 50% of contribution is made by the junior researcher(s).
PROGRAM COMMITTEE CHAIRS
------------------------
Marco Gaboardi, Boston University
Femke van Raamsdonk, Vrije Universiteit Amsterdam
Email: fscd2023 at easychair.org
PROGRAM COMMITTEE
-----------------
Martin Avanzini, INRIA
Patrick Bahr, ITU Copenhagen
Pablo Barenbaum, University of Quilmes (CONICET) & ICC
Filippo Bonchi, University of Pisa
Sabine Broda, University of Porto
Valeria De Paiva, Topos Institute
Andrej Dudenhefner, TU Dortmund
Santiago Escobar, Universitat Politècnica de València
Claudia Faggian, University of Paris (IRIF)
Frank (Peng) Fu, Dalhousie University
Silvio Ghilardi, University of Milano
Clemens Grabmayer, GSSI or Gran Sasso Science Institute
Nao Hirokawa, JAIST
Mirai Ikebuchi, National Institute of Informatics
Ambrus Kaposi, Eotvos Lorand University
Ian Mackie, University of Sussex
Radu Mardare, University of Strathclyde
Aart Middeldorp, University of Innsbruck
Anders Mortberg, University of Stockholm
Daniele Nantes-Sobrinho, Imperial College London / University of Brasília
Vincent van Oostrom, Independent researcher
Grigore Rosu, University of Illinois Urbana-Champaign
Luca Roversi, University of Torino
Aleksy Schubert, University of Warsaw
Jakob G. Simonsen, University of Copenhagen
Alwen Tiu, Australian National University
Valeria Vignudelli, CNRS/ENS Lyon
Johannes Waldmann, HTWK Leipzig
Sarah Winkler, University of Bolzano
CONFERENCE CHAIR
----------------
Daniele Gorla, University of Rome - Sapienza
WORKSHOP CHAIR
--------------
Ivano Salvo, University of Rome - Sapienza
STEERING COMMITTEE WORKSHOP CHAIR
--------------------------------
Cynthia Kop, Radboud University Nijmegen
PUBLICITY CHAIR
---------------
Carsten Fuhs, Birkbeck, University of London
FSCD STEERING COMMITTEE
-----------------------
Zena Ariola, University of Oregon
Alejandro Díaz-Caro, Quilmes University & ICC/CONICET
Amy Felty, University of Ottawa
Carsten Fuhs, Birkbeck, University of London
Herman Geuvers (Chair), Radboud University Nijmegen
Silvia Ghilezan, University of Novi Sad
Jürgen Giesl, RWTH Aachen University
Stefano Guerrini, Université de Paris 13
Delia Kesner, Université de Paris Diderot
Naoki Kobayashi, University of Tokyo
Cynthia Kop, Radboud University Nijmegen
Luigi Liquori, Inria
Daniele Nantes, Imperial College London / University of Brasília
(Apologies for the cross postings.)
--------------------------------------------------------------------
Call for Workshop and Tutorial Proposals
- FSCD 2023, 8th edition of the International Conference on Formal Structures for Computation and Deduction
(https://easyconferences.eu/fscd2023/)
July 3-6, 2023
- CADE-29, the 29th Conference on Automated Deduction
(https://easyconferences.eu/cade2023/)
July 1-4, 2023
Rome, Italy
We invite proposals for workshops, tutorials or other satellite events, on any topic related to formal structures in computation, deduction and automated reasoning, from theoretical foundations to tools and applications.
FSCD satellite events will take place before the main conference on July 1-2, and CADE satellite events will take place after the main conference on July 4 (afternoon)-5. It is expected that satellite events would run for 1/2, 1 or 2 days (max 1 and 1/2 day for CADE satellite events), and be open to participants of parallel events. Please note overlaps between FSCD workshops and CADE conference and between CADE workshops and FSCD conference (see Important Dates below).
PROPOSALS
--------------------
Proposals must be limited to three pages and should be submitted via easychair:
https://easychair.org/my/conference?conf=fscd23cade29ws
Each proposal should consist of the following two parts.
1) A description part including:
- 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);
- a brief description (up to 120 words) of the event for the website and publicity material.
2) An organisational part including:
- contact information for the workshop organisers;
- proposed affiliated conference;
- estimate of the number of workshop participants;
- proposed format and agenda (e.g. paper presentations, tutorials, demo sessions, etc.)
- potential invited speakers;
- procedures for selecting papers and participants;
- tentative schedule for paper submission and notification of acceptance;
- plans for dissemination, if any (e.g. a journal special issue);
- duration (which may vary from half a day to two days (max 1 and 1/2 days for CADE));
- any other special requirements.
The Organising Committee of FSCD-CADE 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.
The organisers of satellite events are expected to create and maintaina website for the event; handle paper selection, reviewing and acceptance; draw up a tentative programme of talks; advertise their event though specialist mailing lists; prepare the informal pre-proceedings (if applicable) in a timely fashion; and arrange any post-proceedings.
The FSCD-CADE organising committee will handle promotion of the event on the main conference website; integration of the event's programme into the overall timetable; registration of participants; arrangement of an appropriate meeting room; and provision of lunch and coffee breaks for participants.
The organisers may rely on one free registration for every workshop, to be used e.g. for one invited speaker. No other cost will be covered by the local organisation. Workshop organisers are encouraged to find sponsors for financing workshop expenses.
IMPORTANT DATES
--------------------
Main Conferences:
CADE July 1-4, 2023
FSCD July 3-6, 2023
Workshops:
CADE July 4 (afternoon) and 5, 2023
FSCD July 1-2, 2023
Submission of workshop proposals: December 18th, 2022
Notification of success of proposals: December 23rd, 2022
--------------------
Best wishes,
Ivano Salvo
Workshop Chair
CALL FOR PAPERS
Eighth International Conference on
Formal Structures for Computation and Deduction (FSCD 2023)
July 3-6, 2023, Rome, Italy
https://easyconferences.eu/fscd2023/
In-cooperation with ACM SIGLOG and SIGPLAN
IMPORTANT DATES
---------------
All deadlines are midnight anywhere-on-earth (AoE); late submissions will not be considered.
Abstract: January 30, 2023
Submission: February 3, 2023
Rebuttal: March 24-28, 2023
Notification: April 13, 2023
Final version: April 27, 2023
OVERVIEW
--------
FSCD (https://fscd-conference.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 logic, models of computation, semantics and verification in new challenging areas.
The suggested, but not exclusive, list of topics for submission is:
1. Calculi:
- Rewriting systems (string, term, higher-order, graph, conditional, modulo, infinitary, etc.);
- Lambda calculus;
- Logics (first-order, higher-order, equational, modal, linear, classical, constructive, etc.);
- Proof theory (natural deduction, sequent calculus, proof nets, etc.);
- Type theory and logical frameworks;
- Homotopy type theory;
- Quantum calculi.
2. Methods in Computation and Deduction:
- Type systems (polymorphism, dependent, recursive, intersection, session, etc.);
- Induction, coinduction;
- Matching, unification, completion, orderings;
- Strategies (normalization, completeness, etc.);
- Tree automata;
- Model building and model checking;
- Proof search and theorem proving;
- Constraint solving and decision procedures.
3. Semantics:
- Operational semantics and abstract machines;
- Game Semantics and applications;
- Domain theory and categorical models;
- Quantitative models (timing, probabilities, etc.);
- Quantum computation and emerging models in computation.
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;
- Proof assistants and interactive theorem provers;
- Applications in industry;
- Applications of formal systems in other sciences;
- Applications of formal systems in education.
6. Formal Systems for Semantics and Verification in new challenging areas:
- Certification;
- Security;
- Blockchain protocols;
- Data bases;
- Deep learning and machine learning algorithms;
- Planning.
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.
SPECIAL ISSUE
-------------
We aim to have a special issue of Logical Methods in Computer Science of selected papers. More details will be provided later.
SUBMISSION GUIDELINES
---------------------
The submission site is:
https://easychair.org/conferences/?conf=fscd2023
Submissions must be formatted using the LIPIcs style files (https://submission.dagstuhl.de/series/details/5#author) and submitted via EasyChair.
Submissions can be made in two categories. Regular research papers are limited to 15 pages, excluding references and appendices. They must present original research which is unpublished and not submitted elsewhere. System descriptions are limited to 15 pages, excluding references. Shorter papers are welcome and will be given equal consideration.
A system description must present new software tools, or significantly new versions of such tools, in which FSCD topics play an important role. An archive of the code with instructions on how to install and run the tool must be submitted. In addition, a webpage where the system can be experimented with should be provided.
One author of each accepted paper is expected to register and present the work in person at the conference. In case that this is not possible for some unforeseen reason, online presentation will be arranged, but in person registration will still be required.
BEST PAPER AWARD BY JUNIOR RESEARCHERS
--------------------------------------
The program committee will select a paper in which at least one author is a junior researcher, i.e. either a student or whose PhD award date is less than three years from the first day of the meeting. When submitting the paper, other authors should declare to the PC Chair that at least 50% of contribution is made by the junior researcher(s).
PROGRAM COMMITTEE CHAIRS
-----------------------
Marco Gaboardi, Boston University
Femke van Raamsdonk, Vrije Universiteit Amsterdam
Email: fscd2023 at easychair.org
PROGRAM COMMITTEE
-----------------
Martin Avanzini, INRIA
Patrick Bahr, ITU Copenhagen
Pablo Barenbaum, University of Quilmes (CONICET) & ICC
Filippo Bonchi, University of Pisa
Sabine Broda, University of Porto
Valeria De Paiva, Topos Institute
Andrej Dudenhefner, TU Dortmund
Santiago Escobar, Universitat Politècnica de València
Claudia Faggian, University of Paris (IRIF)
Frank (Peng) Fu, Dalhousie University
Silvio Ghilardi, University of Milano
Clemens Grabmayer, GSSI or Gran Sasso Science Institute
Nao Hirokawa, JAIST
Mirai Ikebuchi, National Institute of Informatics
Ambrus Kaposi, Eotvos Lorand University
Ian Mackie, University of Sussex
Radu Mardare, University of Strathclyde
Aart Middeldorp, University of Innsbruck
Anders Mortberg, University of Stockholm
Daniele Nantes-Sobrinho, Imperial College London / University of Brasília
Vincent van Oostrom, Independent researcher
Grigore Rosu, University of Illinois Urbana-Champaign
Luca Roversi, University of Torino
Aleksy Schubert, University of Warsaw
Jakob G. Simonsen, University of Copenhagen
Alwen Tiu, Australian National University
Valeria Vignudelli, CNRS/ENS Lyon
Johannes Waldmann, HTWK Leipzig
Sarah Winkler, University of Bolzano
CONFERENCE CHAIR
----------------
Daniele Gorla, University of Rome - Sapienza
WORKSHOP CHAIR
--------------
Ivano Salvo, University of Rome - Sapienza
STEERING COMMITTEE WORKSHOP CHAIR
--------------------------------
Cynthia Kop, Radboud University Nijmegen
PUBLICITY CHAIR
---------------
Carsten Fuhs, Birkbeck, University of London
FSCD STEERING COMMITTEE
-----------------------
Zena Ariola, University of Oregon
Alejandro Díaz-Caro, Quilmes University & ICC/CONICET
Amy Felty, University of Ottawa
Carsten Fuhs, Birkbeck, University of London
Herman Geuvers (Chair), Radboud University Nijmegen
Silvia Ghilezan, University of Novi Sad
Jürgen Giesl, RWTH Aachen University
Stefano Guerrini, Université de Paris 13
Delia Kesner, Université de Paris Diderot
Naoki Kobayashi, University of Tokyo
Cynthia Kop, Radboud University Nijmegen
Luigi Liquori, Inria
Daniele Nantes, Imperial College London / University of Brasília
Dear all,
I am preparing my course at ISR 22
about "constraint programming for analysis of rewriting".
(plan: https://www.imn.htwk-leipzig.de/~waldmann/talk/22/isr/ )
If you are using SAT/SMT in your termination prover -
how do you actually do it?
- how do you write the constraints
- what logics do you use
- how do you manage the (external) solver process
Example answers for matchbox - see below.
I'd appreciate brief answers here on the list
(or in email, and I can later summarize back)
perhaps with pointers to source and publications.
If there are no (current) publications - then we could write one?
Thanks - Johannes.
For example - for matchbox, the constraints are really
QF_NIA (standard matrices) and QF_LRA (arctic)
but I am not writing them as such,
but instead I am using an (eager) bit-blasting translation to SAT,
with the Ersatz library. That library neatly solves the
memoization problem (with hidden unsafePerformIO
https://hackage.haskell.org/package/ersatz-0.4.12/docs/src/Ersatz.Problem.h…
)
so I can write the constraints in a functional way
(e.g., unknown numbers, and matrices, are instances of Num,
so `sum` automatically works, etc.)
For actual SMT writing, a nicely typed embedded DSL is
https://hackage.haskell.org/package/smtlib2-1.0/docs/Language-SMTLib2.html
but it seems unmaintained, and I found it hard to add patches
(necessary because of changes in SMTLIB format specs)
I recently looked into https://hackage.haskell.org/package/simple-smt
but it requires some ugly monadic code, cf. evaluate_rule(_arc)
https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/blob/457-find-a…
For actual SMT solving - I found these problems:
- QF_NIA (polynomial integer arithmetic) is hopeless,
we could use QF_BV (bitvectors) instead
but their arithmetic operators are silently overflowing
(it's modular arithmetic) so it requires extra (Boolean) programming
- QF_LRA is nice, but for each arctic number, I need an extra Boolean
(to encode MinusInfinity)
in all, the Boolean aspect seems to dominate,
so I could bit-blast directly (which I do).
Perhaps it's time for an arctic theory solver ...
Oh, and another technical point - I prefer to call the solver
via its (C) API, instead of writing to file, and calling an external
process. It seems faster - and I can stop/kill the solver (process)
much more reliably. But - while the textual input/output format is
fixed, those binary interfaces require extra (solver-specific) code
that will bit-rot quickly. SAT solvers seem to settle on IPASIR,
perhaps there's a similar standard emerging for SMT?
Dear Akihisa,
for SRS-Standard (certified), for several benchmarks,
example ICFP_2010/4991.xml, these results are displayed:
- matchbox: "YES (without \checkmark)"
https://www.starexec.org/starexec/services/jobs/pairs/567222906/stdout/1?li…
- ttt2: "post-processor error" (post processor timeout after 15 min)
https://www.starexec.org/starexec/services/jobs/pairs/567222903/log
these are logically the same thing?
(both did produce a certificate?)
Ah - noh, for matchbox, the certifier did not time-out,
but "certification-err Stack space overflow: current size 8388608..."
Locally, I am not getting this error (certification succeeds
in 50 seconds for matchbox' certificate, 55 seconds for ttt2's)
I am using ceta-postproc (contains CeTA-2.42) compiled with ghc-9.0.2
- Johannes.
Dear all,
Following some requests, the workshop for termination will be held
tomorrow and Friday in a *hybrid* manner (with mostly live talks, but
the possibility for remote attendance). Hence, for those of you who are
not in Haifa, remote participation is possible, and we will do our best
to support as smooth an experience as possible.**
The program is available at
https://easychair.org/smart-program/FLoC2022/WST-index.html ; in short,
Thursday is dedicated to theory presentations, and Friday to tools and
the termination competition.
Zoom data:
* Thursday:
o https://radbouduniversity.zoom.us/j/85852431972?pwd=Y1ZwY1RPeUU2MzUwWU9lNXZ…
(09:00--16:30 Haifa time; the meeting opens a bit earlier for
setting up and testing)
o Meeting ID: 858 5243 1972
Passcode: 928647
* Friday:
o https://radbouduniversity.zoom.us/j/89259808849?pwd=eHF2a1BWTWwrR3pmOS9tbzB…
(10:00--15:30 Haifa time)
o Meeting ID: 892 5980 8849
o Passcode: 792570
Hope to see you there!
Cynthia.
** Though this comes with a disclaimer: we can only offer our best
effort, like the other hybrid FLoC workshops. The local setup is not
geared towards hybrid, so it is very possible that there will be some
issues with the network, sound quality or screen sharing.
Dear all,
some jobs of the first run have been started. Please monitor via:
https://termcomp.github.io/Y2022/
(Not all jobs because of the popular permission problems.)
Good luck!
Akihisa