PROGRAM
Days: Wednesday, July 1st Thursday, July 2nd Friday, July 3rd Saturday, July 4th
Wednesday, July 1st
View this program: with abstractssession overviewtalk overview
11:30-12:30 Session 1: FSCD-IJCAR Invited Speaker: R. Thiemann. (all times are in CEST timezone - UTC+2)
Chair:
11:30 | Certifying Termination Proofs: From Term Rewriting to SMT Solving and Back (abstract) |
12:30-13:00Coffee Break
13:00-14:30 Session 2A: Rewriting. (all times are in CEST timezone - UTC+2)
Chair:
13:00 | A Fast Decision Procedure for Uniqueness of Normal Forms w.r.t. Conversion of Shallow Term Rewriting Systems (abstract) |
13:30 | Strongly Normalizing Higher-Order Relational Queries (abstract) |
14:00 | WANDA - a Higher Order Termination Tool - System description (abstract) |
13:00-15:00 Session 2B: Program Logics and Verification. (all times are in CEST timezone - UTC+2)
Chair:
13:00 | Symbolic Execution Game Semantics (abstract) |
13:30 | A Probabilistic Higher-order Fixpoint Logic (abstract) |
14:00 | Refining Constructive Hybrid Games (abstract) |
14:30 | On Average-Case Hardness of Higher-Order Model Checking (abstract) |
15:15-16:15 Session 3: IJCAR-FSCD Invited Speaker: J. Harrison. (all times are in CEST timezone - UTC+2)
Chair:
15:15 | Adventures in Verifying Arithmetic (abstract) |
Thursday, July 2nd
View this program: with abstractssession overviewtalk overview
13:00-14:00 Session 4: Invited Speaker: S. Ronchi Della Rocca. (all times are in CEST timezone - UTC+2)
Chair:
13:00 | A foundational lambda calculus for probabilistic computation (abstract) |
14:00-14:30Coffee Break
14:30-16:30 Session 5A: Grammars, Automata and Decision Trees. (all times are in CEST timezone - UTC+2)
Chair:
14:30 | Adaptive Non-linear Pattern Matching Automata (abstract) |
15:00 | Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars (abstract) |
15:30 | Unital Anti-unification: Type and Algorithms (abstract) |
16:00 | Undecidability of Semi-unification on a Napkin *** Best paper by a junior researcher (abstract) |
14:30-16:30 Session 5B: Categorical Semantics and Structures. (all times are in CEST timezone - UTC+2)
Chair:
14:30 | Towards Constructive Hybrid Semantics (abstract) |
15:00 | String diagrams for optics (abstract) |
15:30 | A Profunctorial Scott Semantics (abstract) |
16:00 | Comprehension and quotient structures in the language of 2-categories (abstract) |
16:30-17:00Coffee Break
17:00-18:30 Session 6A: Theorem Proving Algorithms and Constraint Solving. (all times are in CEST timezone - UTC+2)
Chair:
17:00 | Constraint Solving over Multiple Similarity Relations (abstract) |
17:30 | A Type Checker for a Logical Framework with Union and Intersection Types - System description (abstract) |
18:00 | Efficient Full Higher-Order Unification *** Best paper by junior researchers (abstract) |
17:00-18:00 Session 6B: Program Specification. (all times are in CEST timezone - UTC+2)
Chair:
17:00 | Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi - System description (abstract) |
17:30 | Modules over monads and operational semantics (abstract) |
Friday, July 3rd
View this program: with abstractssession overviewtalk overview
13:00-14:00 Session 7: Invited speaker: A. Pitts (all times are in CEST timezone - UTC+2)
Chair:
13:00 | Quotients in Dependent Type Theory (abstract) |
14:00-14:30Coffee Break
14:30-16:30 Session 8A: Dependent Types and Rewriting. (all times are in CEST timezone - UTC+2)
Chair:
14:30 | Type safety of rewriting rules in dependent types (abstract) |
15:00 | Encoding Agda Programs using Rewriting (abstract) |
15:30 | The new rewriting engine of Dedukti - System description (abstract) |
16:00 | A Syntax for Mutual Inductive Families (abstract) |
14:30-16:00 Session 8B: Concurrency. (all times are in CEST timezone - UTC+2)
Chair:
14:30 | Pomsets with Boxes: Protection, Separation, and Locality in Concurrent Kleene Algebra (abstract) |
15:00 | Conditional Bisimilarity for Reactive Systems (abstract) |
15:30 | Resource-Aware Session Types with Arithmetic Refinements *** Best system description by a junior researcher (abstract) |
Saturday, July 4th
View this program: with abstractssession overviewtalk overview
13:00-14:30 Session 10A: Calculi and Translations (all times are in CEST timezone - UTC+2)
Chair:
13:00 | Semi-Axiomatic Sequent Calculus (abstract) |
13:30 | A Gentzen-style monadic translation of Goedel's System T (abstract) |
14:00 | The difference lambda-calculus: a language for difference categories. (abstract) |
13:00-14:30 Session 10B: Effects. (all times are in CEST timezone - UTC+2)
Chair:
13:00 | A Reflection on Continuation-Composing Style (abstract) |
13:30 | Data-flow analyses as effects and graded monads (abstract) |
14:00 | A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers (abstract) |
14:30-15:00Coffee Break
15:00-16:00 Session 11: Invited speaker: B. Pientka. (all times are in CEST timezone - UTC+2)
Chair:
15:00 | A Modal Analysis of Metaprogramming (abstract) |