The Coq mailing list

[Steve Awodey <awodey AT cmu.edu>]

Unsubscribe 

> On Jan 17, 2023, at 22:36, coq-club-request AT inria.fr wrote:
> 
> coq-club digest Wed, 18 Jan 2023
> 
> Table of contents:
> 
> * 1 - [Coq-Club] Call for Papers: Logical Frameworks and Meta-Languages:
>  Theory and Practice (LFMTP'23) - Carlos Olarte <carlos.olarte AT gmail.com>
> * 2 - [Coq-Club] CADE-29 Call for Papers - geoff AT cs.miami.edu
> * 3 - [Coq-Club] UNIF 2023 Call for Papers - Christophe Ringeissen
>  <christophe.ringeissen AT loria.fr>
> * 4 - [Coq-Club] GCM 2023: First call for papers - Jens Kosiol
>  <kosiolje AT mathematik.uni-marburg.de>
> * 5 - [Coq-Club] Coq Platform 2022.09.1 release with Coq 8.16.1 - Théo
>  Zimmermann <theo.zimmermann AT telecom-paris.fr>
> * 6 - [Coq-Club] Volunteer co-maintainer needed for Docker-Coq - Théo
>  Zimmermann <theo.zimmermann AT telecom-paris.fr>
> 
> ----------------------------------------------------------------------
> 
> Message-ID:
> <CAFh-QQE9xGhxoEP6kDTmxNwfEJWbE8Exd+qNngXNiSpYfULY0g AT mail.gmail.com>
> Date: Thu, 12 Jan 2023 10:57:54 +0100
> From: Carlos Olarte <carlos.olarte AT gmail.com>
> Subject: [Coq-Club] Call for Papers: Logical Frameworks and Meta-Languages:
> Theory and Practice (LFMTP'23)
> 
> ===============================================================
> 
>             Call for papers -- LFMTP 2023
> 
>           Logical Frameworks and Meta-Languages:
>                   Theory and Practice
> 
>             Rome, Italy -- July 2nd, 2023
>               Affiliated with FSCD 2023
> 
>              https://lfmtp.org/workshops/2023
> 
> ===============================================================
> 
> Logical frameworks and meta-languages form a common substrate for
> representing, implementing and reasoning about a wide variety of
> deductive systems of interest in logic and computer science. Their
> design, implementation and their use in reasoning tasks, ranging from
> the correctness of software to the properties of formal systems,
> have been the focus of considerable research over the last two decades.
> This workshop will bring together designers, implementors and
> practitioners to discuss various aspects impinging on the structure and
> utility of logical frameworks, including the treatment of variable
> binding, inductive and co-inductive reasoning techniques and the
> expressiveness and lucidity of the reasoning process.
> 
> LFMTP 2023 will provide researchers a forum to present state-of-the-art
> techniques and discuss progress in areas such as the following:
> 
> * Encoding and reasoning about the meta-theory of programming languages,
>  logical systems and related formally specified systems.
> 
> * Theoretical and practical issues concerning the treatment of variable
>  binding, especially the representation of, and reasoning about,
>  datatypes defined from binding signatures.
> 
> * Logical treatments of inductive and co-inductive definitions and
>  associated reasoning techniques, including inductive types of higher
>  dimension in homotopy type theory.
> 
> * Graphical languages for building proofs, applications in geometry,
>  equational reasoning and category theory.
> 
> * New theory contributions: canonical and substructural frameworks,
>  contextual frameworks, proof-theoretic foundations supporting
>  binders, functional programming over logical frameworks,
>  homotopy and cubical type theory.
> 
> * Applications of logical frameworks: proof-carrying architectures,
>  proof exchange and transformation, program refactoring, etc.
> 
> * Techniques for programming with binders in functional programming
>  languages such as Haskell, OCaml or Agda, and logic programming
>  languages such as lambda Prolog or Alpha-Prolog.
> 
> The workshop's program will include contributed and invited talks.
> We hope that LFMTP takes place physically in Rome, but online
> participation will be possible and may even be necessary.
> 
> ## Important Dates
> 
> Abstract submission deadline: April 10
> Paper submission deadline: April 20
> Notification to authors: May 20
> 
> ## Submission
> 
> Submit on EasyChair: https://easychair.org/conferences/?conf=lfmtp23
> 
> All papers must be original and not simultaneously submitted to another
> journal or conference.
> 
> In addition to regular papers, we welcome/encourage the submission of
> "work in progress" reports, in a broad sense. Those do not need to
> report fully polished research results, but should be of interest for
> the community at large.
> 
> Submitted papers should be in PDF, formatted using the EPTCS style
> guidelines (https://info.eptcs.org/). The length is restricted to 15
> pages for regular papers and 8 pages for "work in progress" papers
> (both limits include references).
> 
> ## Proceedings
> 
> A selection of the presented papers will be published online in the
> Electronic Proceedings in Theoretical Computer Science (EPTCS).
> 
> ## Program Committee
> 
> * Roberto Blanco (MPI-SP)
> * Frédéric Blanqui (Inria)
> * Ana Bove (Chalmers University of Technology)
> * Alberto Ciaffaglione, co-chair (Università degli Studi di Udine)
> * Amy Felty (University of Ottawa)
> * Assia Mahboubi (Inria)
> * Narciso Marti-Oliet (Universidad Complutense de Madrid)
> * Gopalan Nadathur (University of Minnesota)
> * Carlos Olarte, co-chair (LIPN, Université Sorbonne Paris Nord)
> * Clément Pit-Claudel (Amazon AWS)
> * Andrei Popescu (University of Sheffield)
> * Claudio Sacerdoti Coen (University of Bologna)
> 
> 
> ------------------------------
> Message-ID: <20230112160650.EE4B8A0464F AT armistead.ccs.miami.edu>
> Date: Thu, 12 Jan 2023 11:06:50 -0500 (EST)
> From: geoff AT cs.miami.edu
> Subject: [Coq-Club] CADE-29 Call for Papers
> 
> ******************************************************************
> 
>                      CALL FOR PAPERS
> 
>    CADE-29: 29th international Conference on Automated Deduction
> 
>                  Sapienza University of Rome
>                 Rome, Italy, 1-5 July 2023
> 
>              https://easyconferences.eu/cade2023
> 
> ******************************************************************
> 
> -- Overview --
> 
> CADE is the major international forum for presenting research on all aspects
> of
> automated deduction. High-quality submissions on the general topic of
> automated
> deduction, including logical foundations, theory and principles, 
> applications
> in and beyond computer science and mathematics, and implementations of
> automated
> reasoning systems are solicited. CADE-29 aims to present research that
> reflects
> the broad range of interesting and relevant topics in automated deduction.
> 
> CADE-29 is in cooperation with ACM SIGLOG.
> 
> -- Venue --
> 
> CADE-29 and affiliated satellite events will take place in Rome, Italy and
> will
> be co-located with FSCD 2023.
> 
> -- Publication --
> 
> CADE-29 proceedings will be published in Springer's Lecture Notes in
> Artificial
> Intelligence series in Gold Open Access mode at a CADE special rate of
> ���200.00
> per paper. Funding will be available for authors of accepted papers who 
> cannot
> cover the ���200 fee.
> 
> -- Special Issue --
> 
> The authors of a selection of the best CADE-29 papers will be invited to
> submit
> an extended version of their paper after the conference, to be published in 
> a
> special issue of the Journal of Automated Reasoning.
> 
> -- Submission Guidelines --
> 
> Submissions can be made in two categories:
> 
> - **Regular papers**. Up to 15 pages in LNCS style, excluding references.
>  Proofs of theoretical results that do not fit in the page limit may be
>  provided in an appendix.
> 
> - **Short papers**. This includes system descriptions, user experiences, 
> case
>  studies and domain models. Up to 10 pages in LNCS style, excluding
>  references.
> 
> Reviewers may consider material provided in appendices, but submissions must
> be
> self-contained within the page limit. Submissions must be unpublished and 
> not
> submitted for publication elsewhere. They will be judged on relevance,
> originality, significance, correctness, and readability. If software or data
> is
> relevant to a paper, a link that provides access to the software/data must 
> be
> provided to enable reproduction of results.
> 
> The review process will include a feedback/rebuttal period where authors 
> will
> have the option to respond to reviewer comments. The PC chairs may solicit
> further reviews after the rebuttal period. Selected accepted papers will be
> considered by Program Committee for the CADE Best Paper Award.
> 
> Papers must be submitted to https://easychair.org/conferences/?conf=cade29
> 
> All submission must be formatted in the LNCS style and must include the 
> ORCID
> id of at least the corresponding author, and preferably of all authors.
> 
> -- Important Dates --
> 
> Abstract deadline:      February 27, 2023
> Submission deadline:    March 6, 2023
> Rebuttal phase:         April 18-20, 2023
> Notification:           May 3, 2023
> Final version:          May 24, 2023
> Main Conference:        July 1-4, 2023
> Satellite events:       July 4-5, 2023
> 
> -- Program Committee Chairs --
> Brigitte Pientka, MacGill University
> Cesare Tinelli, The University of Iowa
> 
> -- Policies--
> CADE implements the ACM policy against harassment.
> 
> -- Contacts --
> All questions about CADE-29 paper submissions should be emailed to the
> PC Chairs (cade29 at easychair.org).
> 
> 
> ------------------------------
> Message-ID: <78C9174A-6017-425E-9FEB-BAFEB1419D92 AT loria.fr>
> Date: Fri, 13 Jan 2023 13:38:37 +0100
> From: Christophe Ringeissen <christophe.ringeissen AT loria.fr>
> Subject: [Coq-Club] UNIF 2023 Call for Papers
> 
> [Apologies for multiple copies]
> 
> =============================================================
>               Call for Papers
>                  UNIF 2023
>        The 37th International Workshop on Unification
>              Rome, Italy, July 2, 2023
>       A satellite workshop of CADE/FSCD, affiliated with FSCD
>          https://project.inria.fr/unif2023
> =============================================================
> 
> 
> UNIF 2023 is the 37th event in a series of international meetings
> devoted to unification theory and its applications. Unification is
> concerned with the problem of identifying terms, finding solutions for
> equations, or making formulas equivalent. It is a fundamental process
> used in a number of fields of computer science, including automated
> reasoning, term rewriting, logic programming, natural language
> processing, program analysis, types, etc.
> 
> The International Workshop on Unification (UNIF) is a yearly forum for
> researchers in unification theory and related fields to meet old and
> new colleagues, to present recent (even unfinished) work, and to
> discuss new ideas and trends. It is also a good opportunity for young
> researchers and scientists working in related areas to get an overview
> of the current state of the art in unification theory.
> 
> 
> Topics
> ------
> A non-exhaustive list of topics of interest includes:
> 
>  * syntactic and equational unification
>  * matching
>  * constraint solving
>  * unification in modal, temporal, and description logics
>  * narrowing
>  * disunification
>  * anti-unification
>  * semi-unification
>  * higher-order unification
>  * complexity issues
>  * implementation techniques
>  * applications
> 
> 
> Submission
> ----------
> 
> Short papers or extended abstracts, up to 5 pages in EasyChair style,
> should be submitted electronically as PDF files through the EasyChair
> submission site:
> 
>  https://www.easychair.org/conferences/?conf=unif2023
> 
> Abstracts will be evaluated by the Program Committee regarding their
> significance for the workshop. Accepted abstracts will be presented at
> the workshop and included in the informal proceedings of the workshop,
> available in electronic form.  Based on the number and quality of
> submissions we will decide whether to organize a special journal
> issue.
> 
> 
> Important Dates
> ---------------
>  * Paper Submission:                  April 21, 2023
>  * Author notification:                 May 26, 2023
>  * Final version:                       June 9, 2023
>  * UNIF 2023:                           July 2, 2023
> 
> 
> ------------------------------
> Message-ID: <295eae02-0c6c-71d2-f9df-6afc7c2feead AT mathematik.uni-marburg.de>
> Date: Mon, 16 Jan 2023 14:18:46 +0100
> From: Jens Kosiol <kosiolje AT mathematik.uni-marburg.de>
> Subject: [Coq-Club] GCM 2023: First call for papers
> 
> ********************************************************************************
> ***************************** CALL FOR PAPERS
> ************************************
> ********************************************************************************
> 
> 14th International Workshop on Graph Computation Models (GCM 2023)
> 
> 18-21 July 2023 (exact day TBC)
> 
> Venue: Leicester, UK
> 
> Web site: https://conf.researchr.org/home/staf-2023/gcm-2023
> 
> Part of STAF 2023 (https://conf.researchr.org/home/staf-2023)
> 
> ================================================================================
> 
> Graphs are common mathematical structures which are visual and
> intuitive. They constitute a natural and seamless way for system
> modeling in science, engineering and beyond, including computer science,
> life sciences, business processes, etc. Graph computation models
> constitute a class of very high-level models where graphs are
> first-class citizens. They generalize classical computation models based
> on strings or trees, such as Chomsky grammars or term rewrite systems.
> Their mathematical foundation, in addition to their visual nature,
> facilitates specification, validation and analysis of complex systems. A
> variety of computation models have been developed using graphs and
> rule-based graph transformation. These models include features of
> programming languages and systems, paradigms for software development,
> concurrent calculi, local computations and distributed algorithms, and
> biological and chemical computations.
> 
> The International Workshop on Graph Computation Models aims at bringing
> together researchers interested in all aspects of computation models
> based on graphs and graph transformation. It promotes the
> cross-fertilizing exchange of ideas and experiences among young and
> senior researchers from different communities who are interested in the
> foundations, applications, and implementations of graph computation
> models and related areas.
> 
> --------------------------------------------------------------------------------
> 
> ** IMPORTANT DATES **
> 
> Abstract Submission:    07 May 2023
> Paper Submission:       14 May 2023
> Notification:           12 June 2023
> Final version due:      26 June 2023
> Workshop:               18–21 July 2023 (exact day TBC)
> 
> --------------------------------------------------------------------------------
> 
> ** TOPICS **
> 
> GCM 2023 solicits papers on all aspects of graph computation models.
> This includes, but is not limited to the following topics:
> 
> FOUNDATIONS
> * Models of graph transformation
> * Analysis and verification of graph transformation systems
> * Parallel, concurrent, and distributed graph transformation
> * Term graph rewriting
> * Formal graph languages
> 
> APPLICATIONS
> * Graph-based programming models and visual programming
> * Program analysis and transformation
> * Graph-based machine learning, including graph neural networks and
> models of rule inference
> * Model-driven engineering and model transformation
> * Evolutionary computation; software architectures, validation and evolution
> * Databases
> * Graph-based security models
> * Workflow and business processes
> * Social network analysis
> * Bioinformatics and computational chemistry
> * Quantum computing
> * Case studies
> 
> ---------------------------------------
> 
> ** SUBMISSION TYPES **
> 
> Authors are invited to submit papers in any of the following three
> categories:
> 
> (1) Regular papers of at most 16 pages describing innovative contributions.
> 
> (2) Short papers (work in progress, system descriptions, or position
> papers) of 6 to 12 pages.
> 
> (3) Short announcements of 1 or 2 pages, to be presented as lightning
> talks of 5 minutes.
> 
> Papers in PDF format should be submitted electronically via the
> EasyChair system site (https://easychair.org/conferences/?conf=gcm23).
> Submissions must use the EPTCS LaTeX style (http://style.eptcs.org/).
> Simultaneous submission to other conferences with proceedings, as well
> as submission of material that has already been published elsewhere is
> not allowed for regular and short papers. The page limits include
> references. An optional appendix may be added if this is useful for the
> reviewing process. If a short announcement extensively draws on already
> published work, a copy of that work is to be attached to the submission.
> 
> All submissions will be reviewed by the programme committee; short
> announcements will undergo a lightweight review and mainly be assessed
> for their potential to stir discussion on future research of the
> community. Electronic proceedings will be available at the time of the
> workshop. Selected authors of regular and short papers will be invited
> to contribute to post-proceedings to be published online by Electronic
> Proceedings in Theoretical Computer Science (EPTCS, http://www.eptcs.org/).
> 
> ---------------------------------------
> 
> ** PROGRAMME COMMITTEE **
> 
> Confirmed programme committee members at the time of this call are:
> 
> * Andrea Corradini, Università di Pisa, Italy
> * Rachid Echahed, University of Grenoble - CNRS, France
> * Fabio Gadducci, Università di Pisa, Italy
> * Reiko Heckel, University of Leicester, Germany
> * Tobias Heindel (co-Chair), Heliax GmbH, Germany
> * Berthold Hoffmann, University of Bremen, Germany
> * Barbara König, University of Duisburg-Essen, Germany
> * Jens Kosiol (co-Chair), Philipps-Universität Marburg, Germany
> * Leen Lambers, Brandenburgische Technische Universität
> Cottbus-Senftenberg, Germany
> * Marino Miculan, University of Udine, Italy
> * Mark Minas, Universität der Bundeswehr München, Germany
> * Detlef Plump, University of York, UK
> * Sven Schneider, Hasso-Plattner-Institut, University of Potsdam, Germany
> 
> --------------------------------------------------------------------------------
> 
> ** ORGANISERS **
> 
> * Tobias Heindel (tobias AT heliax.dev)
> * Jens Kosiol (kosiolje AT mathematik.uni-marburg.de)
> 
> For more information, please visit the official workshop website at:
> https://conf.researchr.org/home/staf-2023/gcm-2023
> 
> --------------------------------------------------------------------------------
> 
> 
> ------------------------------
> Message-ID: <4926e29c-de60-c181-adc3-a47a917c6146 AT telecom-paris.fr>
> Date: Tue, 17 Jan 2023 13:41:51 +0100
> From: Théo Zimmermann <theo.zimmermann AT telecom-paris.fr>
> Subject: [Coq-Club] Coq Platform 2022.09.1 release with Coq 8.16.1
> 
> Dear Coq community,
> 
> On behalf of the Coq development team, the release manager of Coq 8.16,
> and the Coq Platform team, we are happy to announce the immediate
> availability of the Coq Platform 2022.09.1 release.
> 
> Release highlights:
> 
> - The latest version of Coq has been updated to 8.16.1, which fixes
> critical soundness bugs with previous versions, and brings other
> improvements (see the Coq release notes
> https://coq.inria.fr/refman/changes.html).
> 
> - Many new packages have been added. In particular, Itauto,
> mathcomp-algebra-tactics and mathcomp-word join the "full" level, and
> MetaCoq, Bedrock2 and Fiat-crypto join the "extended" level. See
> https://github.com/coq/platform/releases/tag/2022.09.1 for the complete
> list of additions.
> 
> - This is the first Coq Platform release which contains a macOS "M1 / M2
> / Apple silicon / ARM" DMG installer.
> 
> The main supported version is Coq 8.16.1.
> 
> Several compatibility versions with Coq 8.12 to 8.15 are available,
> including one for Coq 8.15 with a package collection that tries to be as
> similar as possible to the Coq 8.16.1 pick.
> 
> Installers for Coq 8.16 and Coq 8.15 with the newest package collection
> are available for Windows, macOS, and Linux (Snap).
> 
> You can also install the Coq Platform using opam-based scripts, which
> give you access to the main supported version, as well as any of the
> many compatibility versions.
> 
> To learn about the Coq Platform and get access to the installers, please
> refer to: https://github.com/coq/platform/releases/tag/2022.09.1
> 
> 
> ------------------------------
> Message-ID: <a90f24ea-2aae-94e6-26fb-ccdd4a09acdb AT telecom-paris.fr>
> Date: Tue, 17 Jan 2023 17:40:53 +0100
> From: Théo Zimmermann <theo.zimmermann AT telecom-paris.fr>
> Subject: [Coq-Club] Volunteer co-maintainer needed for Docker-Coq
> 
> Dear Coq-Club subscribers,
> 
> The Coq Team and Coq-community are looking for a volunteer co-maintainer
> of the Docker-Coq project, which provides Docker container images of
> many versions of Coq as a service to Coq users:
> https://github.com/coq-community/docker-coq
> 
> Docker-Coq is an open source project on GitHub under the BSD-3-Clause
> license. It maintains definitions of a set of Docker images that provide
> a basic Coq environment for continuous integration and local use. Thanks
> to the docker-keeper software (https://gitlab.com/erikmd/docker-keeper),
> images built from Docker-Coq definitions are continuously deployed to
> the public Docker registry, where users can pull them without worry of
> rate limitations: https://hub.docker.com/r/coqorg/coq
> 
> Desirable skills:
> 
> - Familiarity with container software like Docker
> - Familiarity with software continuous integration and build automation,
> in particular on GitHub and/or GitLab
> - Basic shell scripting
> - Basic Python programming
> 
> Maintainer core tasks:
> 
> - Create and deploy new Coq Docker definitions to the Docker registry
> after Coq (pre-)releases.
> - Monitor the use of Coq Docker images for continuous integration on
> GitHub/GitLab and rebuild images when necessary.
> - Work with the current Docker-Coq and Docker-Keeper maintainer to
> further develop and automate the toolchain.
> 
> During their tenure, maintainers will be considered part of the Coq Team
> (https://coq.inria.fr/coq-team.html) and credited for their work in
> release notes for Coq releases.
> 
> If you are interested in becoming a maintainer, please respond to the
> following GitHub issue:
> https://github.com/coq-community/manifesto/issues/144
> 
> Please include a brief motivation and a short summary of relevant
> experience. The maintainer will be selected from the issue responders by
> the Coq Team and Coq-community owners.
> 
> 
> ------------------------------
> 
> *********************************************
> 
> End of coq-club Digest Wed, 18 Jan 2023
>