PPDP aims to provide a forum that brings together researchers from the declarative programming communities, including those working in the logic, constraint and functional programming paradigms, but also embracing a variety of other paradigms such as visual programming, executable specification languages, database languages, AI languages and knowledge representation languages used, for example, in the semantic web.
The goal is to stimulate research in the use of logical formalisms and methods for specifying, performing, and analysing computations, including mechanisms for mobility, modularity, concurrency, object-orientation, security, and static analysis. Papers related to the use of declarative paradigms and tools in industry and education are especially solicited.
Submissions are invited on all topics related to declarative programming, from principles to practice, from foundations to applications. Topics of interest include, but are not limited to
Language Design: domain-specific languages; interoperability; concurrency, parallelism and distribution; modules; functional languages; reactive languages; languages with objects; languages for quantum computing; languages inspired by biological and chemical computation; metaprogramming.
Declarative languages in artificial intelligence: logic programming; database languages; knowledge representation languages; probabilistic languages; differentiable languages.
Implementations: abstract machines; interpreters; compilation; compile-time and run-time optimization; memory management.
Foundations: types; logical frameworks; monads and effects; semantics.
Analysis and Transformation: partial evaluation; abstract interpretation; control flow; data flow; information flow; termination analysis; resource analysis; type inference and type checking; verification; validation; debugging; testing.
Tools and Applications: programming and proof environments; verification tools; case studies in proof assistants or interactive theorem provers; certification; novel applications of declarative programming inside and outside of CS; declarative programming pearls; practical experience reports and industrial application; education.
The PC chair will be happy to advise on the appropriateness of a topic.
PPDP 2023 will be held in Cascais, Lisbon, Portugal. Previous symposia were held at Tbilisi (Georgia), Tallinn (Estonia), Bologna (Italy), Porto (Portugal), Frankfurt am Main (Germany), Namur (Belgium), Edinburgh (UK), Siena (Italy), Canterbury (UK), Madrid (Spain), Leuven (Belgium), Odense (Denmark), Hagenberg (Austria), Coimbra (Portugal), Valencia (Spain), Wroclaw (Poland), Venice (Italy), Lisboa (Portugal), Verona (Italy), Uppsala (Sweden), Pittsburgh (USA), Florence (Italy), Montréal (Canada), and Paris (France).
Embedding Quantitative Properties of Call-by-Name and Call-by-Value in a Unifying Framework. This talk explores how the (untyped and typed) theories of Call-by-Name (CBN)and Call-by-Value (CBV) can be unified in a more general framework provided by a Call-by-Push-Value (CBPV) like calculus. Indeed, we first present an untyped calculus, called lambda-bang, which encodes untyped CNB and CBV, both from a static and a dynamic point of view. We then explore these encodings in a typed framework, specified by quantitative (aka non-idempotent intersection) types. Three different (quantitative) properties are discussed. The first one is related to upper bounds for reduction lengths, the second one concerns exact measures for reduction lengths and sizes of normal forms, and the last one is about the inhabitation problem. In all these cases, explained and discussed in the talk, the (quantitative) property for CBN/CBV is inherited from the corresponding one in the lambda-bang calculus.
Unification modulo equational theories in languages with binding operators. Unification (i.e., solving equations between terms) is a key step in the implementation of logic programming languages and theorem provers, and is also used in type inference algorithms for functional languages and as a mechanism to analyse rewrite-based specifications (e.g., to find critical pairs). Matching is a version of unification in which only one of the terms in the equation can be instantiated. Often, operators satisfy equational axioms (e.g., associativity, commutativity), which must be taken into account during the unification or matching process. In addition, when the expressions to be unified involve binding operators (as is the case when representing programs, logics, computation models, etc.), unification and matching algorithms must take into account the alpha-equivalence relation generated by the binders. In this talk, we present matching and unification algorithms for languages that include binding operators as well as operators that satisfy equational axioms, such as associativity and commutativity.
Times in the schedule are WEST (Western European Summer Time), i.e., local to Cascais.
Sunday 22 October 2023 |
|
|---|---|
| 08:55 - 09:00 | Opening of PPDP |
| Session 1 | |
| 09:00 - 09:30 |
A Calculus of Delayed Reductions
Steffen van Bakel, Nicolas Wu and Emma Tye |
| 09:30 - 10:00 |
Typed Equivalence of Labeled Effect Handlers and Labeled Delimited Control Operators
Kazuki Ikemori, Youyou Cong and Hidehiko Masuhara |
| 10:00 - 10:30 |
Comprehending queries over finite maps
Wilmer Ricciotti |
| 10:30 - 11:00 | Coffee Break |
| Session 2 | |
| 11:00 - 12:30 | Invited talk: Delia Kesner Embedding Quantitative Properties of Call-by-Name and Call-by-Value in a Unifying Framework |
| 12:30 - 14:00 | Lunch Break |
| Session 3 | |
| 14:00 - 15:30 |
10-Year Most Influential Paper Talk Coq: the world's best macro assembler? Andrew Kennedy, Nick Benton, Jonas B. Jensen, and Pierre-Evariste Dagand |
| 15:30 - 16:00 | Coffee Break |
| Session 4 | |
| 16:00 - 16:30 |
Type-directed Program Transformation for Constant-Time Enforcement
Gautier Raimondi, Frédéric Besson and Thomas Jensen |
| 16:30 - 17:00 |
Data-Dependent Confidentiality in DCR Graphs
Eduardo Geraldo, João Costa Seco and Thomas Hildebrandt |
Monday 23 October 2023 |
|
|---|---|
| Session 5 | |
| 09:00 - 09:30 |
Multicompatibility for Multiparty-Session Composition
Franco Barbanera, Mariangiola Dezani-Ciancaglini, Lorenzo Gheri and Nobuko Yoshida |
| 09:30 - 10:00 |
Termination in Concurrency, Revisited
Joseph Paulus, Daniele Nantes-Sobrinho and Jorge A. Perez |
| 10:00 - 10:30 |
Polymorphic Typestate for Session Types
Hannes Saffrich and Peter Thiemann |
| 10:30 - 11:00 | Coffee Break |
| Session 6 | |
| 11:10 - 12:10 | Invited talk (joint with LOPSTR): Maribel Fernández Unification modulo equational theories in languages with binding operators |
| 12:30 - 14:00 | Lunch Break |
| Session 7 | |
| 14:00 - 14:30 |
Strongly-Typed Multi-View Stack-Based Computations
Pieter Koopman and Mart Lubbers |
| 14:30 - 15:00 |
Closure Conversion in Little Pieces
Zachary J. Sullivan, Paul Downen and Zena M. Ariola |
| 15:00 - 15:30 |
Additive Cellular Automata Graded-Monadically
Silvio Capobianco and Tarmo Uustalu |
| 15:30 - 16:00 | Coffee Break |
| Session 8 | |
| 16:00 - 16:30 |
Intuitionistic Metric Temporal Logic
Luiz de Sá, Bernardo Toninho and Frank Pfenning |
| 16:30 - 17:00 |
stablekanren: Integrating Stable Model Semantics with miniKanren
Xiangyu Guo, James Smith and Ajay Bansal |
| 17:00 - 17:05 | Closing of PPDP |
Submission page is available via EasyChair.
Selected papers will be invited to the Journal of Functional Programming (JFP) or the Journal of Theory and Practice of Logic Programming (TPLP).
Submissions can be made in three categories: regular Research Papers, System Descriptions, and Experience Reports.
Submissions of Research Papers must present original research which is unpublished and not submitted elsewhere. They must not exceed 12 pages ACM style 2-column (including figures, but excluding bibliography). Work that already appeared in unpublished or informally published workshop proceedings may be submitted (please contact the PC chair in case of questions). Research papers will be judged on originality, significance, correctness, clarity, and readability.
Submission of System Descriptions must describe a working system whose description has not been published or submitted elsewhere. They must not exceed 10 pages and should contain a link to a working system. System Descriptions must be marked as such at the time of submission and will be judged on originality, significance, usefulness, clarity, and readability.
Submissions of Experience Reports are meant to help create a body of published, refereed, citable evidence where declarative programming such as functional, logic, answer-set, constraint programming, etc., is used in practice. They must not exceed 5 pages including references. Experience Reports must be marked as such at the time of submission and need not report original research results. They will be judged on significance, usefulness, clarity, and readability.
Possible topics for an Experience Report include, but are not limited to:
Supplementary material may be provided via a link to an extended version of the submission (recommended), or in a clearly marked appendix beyond the above-mentioned page limits. Reviewers are not required to study extended versions or any material beyond the respective page limit. Material beyond the page limit will not be included in the final published version.
For each paper category, you must use the most recent version of the "Current ACM Master Template" which is available at https://www.acm.org/publications/proceedings-template. The most recent version at the time of writing is 1.75. You must use the LaTeX sigconf proceedings template as the conference organizers are unable to process final submissions in other formats. Authors should note ACM's statement on author's rights which apply to final papers. Submitted papers should meet the requirements of ACM's plagiarism policy.
At least one author of each accepted submission will be expected to attend and present the work at the conference. The pc chair may retract a paper that is not presented. The pc chair may also retract a paper if complaints about the paper's correctness are raised which cannot be resolved by the final paper deadline.
