Program

08:00	Max Heisinger The Networked Uncertainty Principle, or How I Stopped Worrying and Love Local Tracing
08:30	Tom van Dijk Demonstrating Work-stealing with Lace and its Application in Sylvan
09:00	Muhammad Osama GPU SAT Solving
09:30	Giles Reger Hacking Shared Memory Parallelism in Vampire

08:00-09:00 Session 2D: PxTP Workshop: Invited Talk (PxTP-7)

Location: ZoomRoom 2

08:00

Maria Paola Bonancina

Proof Generation in CDSAT

08:00-10:00 Session 2E: ThEdu Workshop: ATPs in Geometry (ThEdu'21)

Location: ZoomRoom 1

08:00	Vesna Marinković and Filip Maric Towards Next Step Guidance in Triangle Construction Problems (abstract) PRESENTER: Vesna Marinković
08:30	Pedro Quaresma and Carlos Reis Four Geometry Problems to Introduce Automated Deduction in Secondary Schools (abstract) PRESENTER: Pedro Quaresma
09:00	Zoltán Kovács and Robert Vajda Symbolic Comparison of Geometric Quantities in GeoGebra (abstract) PRESENTER: Zoltán Kovács
09:30	Crispin Perdue Prooftoys: a Proof Assistant for Beginners (abstract)

09:00-10:00 Session 3: PxTP Workshop: Certifying Transformations (PxTP-7)

Location: ZoomRoom 2

09:00	Quentin Garchery A Framework for Proof-Carrying Logical Transformations (abstract)
09:30	Valentin Blot, Louise Dubois de Prisque, Chantal Keller and Pierre Vial General Automation in Coq through Modular Transformations (abstract)

10:00-10:30Break

10:30-12:00 Session 4A: PVS Tutorial (CADE-28)

Chair:

Paolo Masci

Location: ZoomRoom 4

10:30-12:00 Session 4B: PFOR Tutorial (CADE-28)

Chair:

Stephan Schulz

Location: ZoomRoom 5

10:30-12:00 Session 4C: PDAR Workshop: New Directions (PDAR-21)

Chair:

Anton Wijs

Location: ZoomRoom 3

10:30	Alfons Laarman Parallel Probabilistic Inference
11:00	Michael Rawson Parallel Tricks for Speedy Learned Guidance
11:30	Alex Ozdemir Constraint Solving in the Serverless Cloud

10:30-11:30 Session 4D: PxTP Workshop: Invited Talk (PxTP-7)

Location: ZoomRoom 2

10:30

Giles Reger

Reasoning in Many Logics with Vampire: Everything's CNF in the End

10:30-12:00 Session 4E: ThEdu Workshop: ATPs in Geometry; Isabelle in Education (ThEdu'21)

Location: ZoomRoom 1

10:30	Zoltán Kovács and Jonathan H. Yu Automated Discovery of Geometrical Theorems in GeoGebra (abstract) PRESENTER: Zoltán Kovács
11:00	Jørgen Villadsen, Asta Halkjær From and Patrick Blackburn Teaching Intuitionistic Propositional Logic Using Isabelle (abstract) PRESENTER: Jørgen Villadsen
11:30	Walther Neuper, Klaus Miesenberger, Bernhard Stöger and Reinhard Koutny Make Isabelle Accessible! (abstract) PRESENTER: Walther Neuper

11:30-12:30 Session 5: PxTP Workshop: Use Cases (PxTP-7)

Location: ZoomRoom 2

11:30

Nicolas Magaud

Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant (extended abstract) (abstract)

12:00-12:30Break

12:30-14:00 Session 6A: PVS Tutorial (CADE-28)

Chair:

Paolo Masci

Location: ZoomRoom 4

12:30-14:00 Session 6B: PFOR Tutorial (CADE-28)

Chair:

Stephan Schulz

Location: ZoomRoom 5

12:30-14:00 Session 6C: PDAR Workshop: Discussion (PDAR-21)

This will be a structured discussion session arranged around submitted discussion points. The structure will depend on the number of participants. A list of discussion points will be posted on the PDAR website before the session. If you have a discussion point you would like to raise then please contact the chairs.

Chair:

Giles Reger

Location: ZoomRoom 3

12:30-13:10 Session 6D: PxTP Workshop: Generating and Using Proofs (PxTP-7)

Location: ZoomRoom 2

12:30	Stephan Gocht, Ruben Martins and Jakob Nordstrom Certifying CNF Encodings of Pseudo-Boolean Constraints (extended abstract) (abstract)
12:50	Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa and Pascal Fontaine Alethe: Towards a Generic SMT Proof Format (Extended Abstract) (abstract)

12:30-14:00 Session 6E: ThEdu Workshop: Automated Deduction Educational Applications (ThEdu'21)

Location: ZoomRoom 1

12:30	Adam Pease and Stephan Schulz Learning Theorem Proving by Example - Implementing JavaRes (abstract) PRESENTER: Adam Pease
13:00	John Boyland Evolution of SASyLF 2008-2021 (abstract)
13:30	Pablo Donato, Benjamin Werner and Pierre-Yves Strub A Drag-and-Drop Proof Tactic (abstract) PRESENTER: Pablo Donato

13:15-14:00 Session 7: PxTP Workshop: Business Meeting (PxTP-7)

Location: ZoomRoom 2

14:00-14:30Break

14:30-16:00 Session 8A: PVS Tutorial (CADE-28)

Chair:

Paolo Masci

Location: ZoomRoom 4

14:30-16:00 Session 8B: PFOR Tutorial (CADE-28)

Chair:

Stephan Schulz

Location: ZoomRoom 5

14:30-15:20 Session 8C: ThEdu Workshop: Invited Talk (ThEdu'21)

Location: ZoomRoom 1

14:30

Gilles Dowek

How can we make Formal Proof Teachable?

15:20-16:20 Session 9: ThEdu Workshop: Automated Deduction Educational Applications (ThEdu'21)

Location: ZoomRoom 1

15:20	Ankit Kumar, Andrew Walter and Panagiotis Manolios Automated Grading of Automata with ACL2s (abstract) PRESENTER: Ankit Kumar
15:50	Clemens Eisenhofer and Martin Riener Automated Instantiation of Control Flow Tracing Exercises (abstract) PRESENTER: Clemens Eisenhofer

16:20-16:40 Session 10: ThEdu Workshop: Closing and Bussiness Meeting (ThEdu'21)

Location: ZoomRoom 1

Monday, July 12th

View this program: with abstracts session overview talk overview

07:45-08:00 Session 11: Welcome and Announcements (CADE-28)

Chair:

Marijn Heule

Location: ZoomLobby

08:00-09:00 Session 12: Invited Talk (CADE-28)

Chair:

Pascal Fontaine

Location: ZoomRoom 1

08:00

Mooly Sagiv

Formal Reasoning about Decentralized Financial Applications (abstract)

09:00-10:00 Session 13: Theories (A) (CADE-28)

Chair:

Christopher Lynch

Location: ZoomRoom 1

09:00	Franz Brauße, Konstantin Korovin, Margarita Korovina and Norbert Th. Müller The ksmt calculus is a delta-complete decision procedure for non-linear constraints (abstract)
09:30	Alessandro Cimatti, Alberto Griggio and Gianluca Redondi Universal Invariant Checking of Parametric Systems with Quantifier-Free SMT Reasoning (abstract)

10:00-10:30Break

10:30-12:30 Session 14: Logical Foundations (CADE-28)

Chair:

Kaustuv Chaudhuri

Location: ZoomRoom 1

10:30	Joanna Golińska-Pilarek, Michał Zawidzki and Taneli Huuskonen Tableau-based decision procedure for non-Fregean logic of sentential identity (abstract)
11:00	Christoph Wernhard and Wolfgang Bibel Learning from Łukasiewicz and Meredith: Investigations into Proof Structures (abstract)
11:30	Fabio Papacchini, Cláudia Nalon, Ullrich Hustadt and Clare Dixon Efficient Local Reductions to Basic Modal Logic (abstract)
12:00	Tobias Nipkow and Simon Roßkopf Isabelle's Metalogic: Formalization and Proof Checker (abstract)

12:30-13:00Break

13:00-15:00 Session 15: Intuition and Induction (CADE-28)

Chair:

Stefan Mitsch

Location: ZoomRoom 1

13:00	Mnacho Echenim, Radu Iosif and Nicolas Peltier Unifying Decidable Entailments in Separation Logic with Inductive Definitions (abstract)
13:30	Kaustuv Chaudhuri Subformula Linking for Intuitionistic Logic and Type Theory (abstract)
14:00	Camillo Fiorentini Efficient SAT-based proof search in Intuitionistic Propositional Logic (abstract)
14:30	Vivek Nigam, Giselle Reis, Samar Rahmouni and Harald Ruess Proof Search and Certificates for Evidential Transactions (abstract)

15:00-15:30Break

15:30-16:30 Reception (CADE-28)

The CADE-28 (online) reception, a time to meet and interact with friends and foes in the automated reasoning community. It's open bar (BYO), tasty hors d'oeuvres(BYO), and live entertainment ... there will be five "topical sessions", each led by experts in the topical areas. To start it off the experts will give 5 minute teasers for their topics. Then for the second 30 minutes there will be five breakout ZoomRooms in which the experts will lead and listen to discussion of their topics. People can join and leave the topical rooms, to enjoy some interesting interactions. Remember that the ChatRooms are available if you want head off for a private discussion.

Chair:

Marijn Heule

Location: ZoomLobby

15:30-16:00 Session 16: Topical ZoomRoom Teasers (CADE-28)

Chair:

Geoff Sutcliffe

Location: ZoomRoom 1

15:30	Geoff Sutcliffe Reception Opening
15:35	Ruzica Piskac, Nikolaj Bjørner and Laura Kovacs Newbie's Meeting Place PRESENTER: Ruzica Piskac
15:40	Stephan Schulz and Petar Vukmirović 17 Ways to make an ATP System Fast PRESENTER: Stephan Schulz
15:45	Anders Schlichtkrull and Gabriel Ebner How can Anyone Trust a Theorem Prover? PRESENTER: Anders Schlichtkrull
15:50	Cláudia Nalon and Alexander Steen Step into the Darkside - Non-classical Logics PRESENTER: Cláudia Nalon
15:55	Christoph Benzmüller and David Fuenmayor Law, Morality, Religion, and ATP PRESENTER: Christoph Benzmüller

16:00-16:30 Session 17A: Topical ZoomRoom: Newbie's Meeting Place (CADE-28)

Chair:

Nikolaj Bjørner

Location: ZoomRoom 2

16:00-16:30 Session 17B: Topical ZoomRoom: 17 Ways to make an ATP System Fast (CADE-28)

Chair:

Stephan Schulz

Location: ZoomRoom 3

16:00-16:30 Session 17C: Topical ZoomRoom: How can Anyone Trust a Theorem Prover? (CADE-28)

Chair:

Anders Schlichtkrull

Location: ZoomRoom 4

16:00-16:30 Session 17D: Topical ZoomRoom: Step into the Darkside - Non-classical Logics (CADE-28)

Chair:

Cláudia Nalon

Location: ZoomRoom 5

16:00-16:30 Session 17E: Topical ZoomRoom: Morality, Religion, Law, and ATP (CADE-28)

Chair:

Christoph Benzmüller

Location: ZoomRoom 6

Tuesday, July 13th

View this program: with abstracts session overview talk overview

07:45-08:00 Session 18: Announcements (CADE-28)

Chair:

Marijn Heule

Location: ZoomLobby

08:00-10:00 Session 19: Theory in Practice (CADE-28)

Chair:

Nachum Dershowitz

Location: ZoomRoom 1

08:00	Lee Barnett and Armin Biere Non-Clausal Redundancy Properties (abstract)
08:30	Akihisa Yamada Multi-Dimensional Interpretation Methods for Termination of Term Rewriting (abstract)
09:00	Christian Alrabbaa, Franz Baader, Stefan Borgwardt, Patrick Koopmann and Alisa Kovtunova Finding Good Proofs for Description Logic Entailments Using Recursive Quality Measures (abstract)
09:30	Franz Baader, Patrick Koopmann, Francesco Kriegel and Adrian Nuradiansyah Computing Optimal Repairs of Quantified ABoxes w.r.t. Static EL TBoxes (abstract)

10:00-10:30Break

10:00-16:30 Session 20: The CADE-28 ATP System Competition (CASC-28) (CADE-28)

Chair:

Geoff Sutcliffe

Location: ZoomRoom 2

10:30-12:30 Session 21: Inference (CADE-28)

Chair:

Giles Reger

Location: ZoomRoom 1

10:30	Fajar Haifani, Sophie Tourret and Christoph Weidenbach Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance (abstract)
11:00	Gabriel Ebner, Jasmin Blanchette and Sophie Tourret A Unifying Splitting Framework (abstract)
11:30	Petra Hozzová, Laura Kovács and Andrei Voronkov Integer Induction in Saturation (abstract)
12:00	Visa Nummelin, Alexander Bentkamp, Sophie Tourret and Petar Vukmirović Superposition with First-Class Booleans and Inprocessing Clausification (abstract)

12:30-13:00Break

13:00-15:00 Session 22: Implementation (CADE-28)

Chair:

Stephan Schulz

Location: ZoomRoom 1

13:00	Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret and Petar Vukmirović Superposition for Full Higher-Order Logic (abstract)
13:30	Petar Vukmirović, Alexander Bentkamp, Jasmin Blanchette, Simon Cruanes, Visa Nummelin and Sophie Tourret Making Higher-Order Superposition Work (abstract)
14:00	Randal Bryant and Marijn Heule Dual Proof Generation for Quantified Boolean Formulas with a BDD-Based Solver (abstract)
14:30	Hans-Jörg Schurr, Mathias Fleury and Martin Desharnais Reliable Reconstruction of Fine-Grained Proofs in a Proof Assistant (abstract)

15:00-15:30Break

15:30-16:30 Session 23: Invited Talk (CADE-28)

Chair:

Geoff Sutcliffe

Location: ZoomRoom 1

15:30

Guido Governatori

Computational Law: Automated Reasoning in the Legal Domain

Wednesday, July 14th

View this program: with abstracts session overview talk overview

07:45-08:00 Session 24: Announcements (CADE-28)

Chair:

Marijn Heule

Location: ZoomLobby

08:00-09:00 Session 25: Invited Talk (CADE-28)

Chair:

Andre Platzer

Location: ZoomRoom 1

08:00

Liron Cohen

Non-well-founded Deduction for Induction and Coinduction (abstract)

09:00-10:00 Session 26: Theories (B) (CADE-28)

Chair:

Laura Kovacs

Location: ZoomRoom 1

09:00	Ying Sheng, Yoni Zohar, Christophe Ringeissen, Andrew Reynolds, Clark Barrett and Cesare Tinelli Politeness and Stable Infiniteness: Stronger Together (abstract)
09:30	Dohan Kim and Christopher Lynch Equational Theorem Proving Modulo (abstract)

10:00-10:30Break

10:30-12:30 Session 27: Applications in Systems (CADE-28)

Chair:

Tanel Tammet

Location: ZoomRoom 1

10:30	Emre Yolcu, Scott Aaronson and Marijn Heule An Automated Approach to the Collatz Conjecture (abstract)
11:00	Runqing Xu, Liming Li and Bohua Zhan Verified interactive computation of definite integrals (abstract)
11:30	Emery Neufeld, Ezio Bartocci, Agata Ciabattoni and Guido Governatori A Normative Supervisor for Reinforcement Learning Agents (System Description) (abstract)
11:45	Ryan Krueger, Jesse Michael Han and Daniel Selsam Automatically Building Diagrams for Olympiad Geometry Problems (System Description) (abstract)
12:00	Peter Baumgartner The Fusemate Logic Programming System (System Description) (abstract)

12:30-13:00Break

13:00-16:10 Session 28: Awards (CADE-28)

Chair:

Christoph Weidenbach

Location: ZoomRoom 1

13:00	Marijn Heule, André Platzer, Pascal Fontaine and Maria Paola Bonacina Awards: Woody Bledsoe, Best Papers, Bill McCune, Skolem
14:15	Andrei Voronkov 2020 Herbrand Award
14:25	Franz Baader Unification, Combination, Description Logics, and All That (abstract)
15:05	Christoph Weidenbach Break
15:15	Jürgen Giesl 2021 Herbrand Award
15:25	Tobias Nipkow Isabelle: Growing and Applying a Proof Assistant

Thursday, July 15th

View this program: with abstracts session overview talk overview

07:45-08:00 Session 29: Announcements (CADE-28)

Chair:

Marijn Heule

Location: ZoomLobby

08:00-10:00 Session 30: System Descriptions and Competition Reports (CADE-28)

Chair:

Peter Baumgartner

Location: ZoomRoom 1

08:00	Nicholas Smallbone Twee: an equational theorem prover (System Description) (abstract)
08:15	Adrian De Lon, Peter Koepke, Anton Lorenzen, Adrian Marti, Marcel Schütz and Makarius Wenzel The Isabelle/Naproche Natural Language Proof Assistant (System Description) (abstract)
08:30	Leonardo de Moura and Sebastian Ullrich The Lean 4 Theorem Prover and Programming Language (System Description) (abstract)
08:45	Jacob Errington, Junyoung Jang and Brigitte Pientka Harpoon: Mechanizing Metatheory Interactively (System Description) (abstract)
09:00	Geoff Sutcliffe The CADE-28 ATP System Competition (CASC-28) Results (abstract)
09:30	Akihisa Yamada Termination and Complexity Competition Results (abstract)

10:00-10:30Break

10:30-12:00 Session 31: ATP+AI (CADE-28)

Chair:

Cezary Kaliszyk

Location: ZoomRoom 1

10:30	Tanel Tammet, Dirk Draheim and Priit Järv Confidences for Commonsense Reasoning (abstract)
11:00	Filip Bártek and Martin Suda Neural Precedence Recommender (abstract) PRESENTER: Filip Bártek
11:30	Martin Suda Improving ENIGMA-Style Clause Selection While Learning From History (abstract)

12:00-12:30Break

12:30-13:30 Session 32: Invited Talk (CADE-28)

Chair:

Randal Bryant

Location: ZoomRoom 1

12:30

Markus N. Rabe and Christian Szegedy

Towards the Automatic Mathematician (abstract)

13:30-14:00Break

14:00-15:00 Session 33: CADE Business Meeting (CADE-28)

Chair:

Christoph Weidenbach

Location: ZoomRoom 1

Friday, July 16th

View this program: with abstracts session overview talk overview

07:45-08:00 Session 34: Welcome and Announcements (CADE-28)

Chair:

Marijn Heule

Location: ZoomLobby

08:00-10:00 Session 35A: Theorem Proving: Theory and Practice (ARCADE 2021)

Chair:

Martin Suda

Location: ZoomRoom 1

08:00	Erika Abraham, James H. Davenport, Matthew England and Gereon Kremer Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic (abstract)
08:30	David Plaisted Search Spaces for Theorem Proving Strategies (abstract)
09:00	Michael Rawson and Giles Reger On Evaluating Theorem Provers (abstract)
09:30	David Plaisted Relevance and Abstraction (abstract)

08:00-10:00 Session 35B: Non-Fregean Logic Tutorial (CADE-28)

Location: ZoomRoom 4

08:00-10:00 Session 35C: Learning to Prove: ... Tutorial (CADE-28)

Location: ZoomRoom 5

08:00-09:00 Session 35D: LFMTP Workshop: Invited Talk (LFMTP 2021)

Chair:

Elaine Pimentel

Location: ZoomRoom 3

08:00

Giselle Reis

Facilitating Meta-Theory Reasoning

08:00-09:00 Session 35E: WST Workshop: Invited Talk (WST 2021)

Chair:

Samir Genaim

Location: ZoomRoom 2

08:00

Amir Ben-Amram

Efficient Computation of Polynomial Resource Bounds for Bounded-Loop Programs (abstract)

09:00-10:00 Session 36A: LFMTP Workshop: Meta-Theory Reasoning (LFMTP 2021)

Chair:

Elaine Pimentel

Location: ZoomRoom 3

09:00	Laila El-Beheiry, Giselle Reis and Ammar Karkour SMLtoCoq: Automated Generation of Coq Specifications and Proof Obligations from SML Programs with Contracts (abstract) PRESENTER: Laila El-Beheiry
09:30	Qinxiang Cao and Xiwei Wu Countability of Inductive Types Formalized in the Object-Logic Level (abstract) PRESENTER: Xiwei Wu

09:00-10:00 Session 36B: WST Workshop: Classical Topics in Termination (WST 2021)

Chair:

Samir Genaim

09:00	Emre Yolcu, Scott Aaronson and Marijn Heule Mixed Base Rewriting for the Collatz Conjecture (abstract)
09:30	Nachum Dershowitz deVrijer’s Measure for SN of λ→ in Scheme (abstract)

10:00-10:30Break

10:30-11:30 Session 37A: TPTP World (ARCADE 2021)

Chair:

Sarah Winkler

Location: ZoomRoom 1

10:30	Geoff Sutcliffe The Expansion, Modernisation, and Future of the TPTP World (abstract)
11:00	Geoff Sutcliffe and David Plaisted Management of the TPTP Problem Set (abstract)

10:30-12:00 Session 37B: Non-Fregean Logic Tutorial (CADE-28)

Location: ZoomRoom 4

10:30-12:00 Session 37C: Learning to Prove: ... Tutorial (CADE-28)

Location: ZoomRoom 5

10:30-12:00 Session 37D: LFMTP Workshop: Foundations (LFMTP 2021)

Chair:

Florian Rabe

Location: ZoomRoom 3

10:30	Johannes Schoisswohl and Laura Kovacs Automating Induction by Reflection (abstract) PRESENTER: Johannes Schoisswohl
11:00	Gilles Dowek Interacting safely with an unsafe environment (abstract)
11:30	David Baelde, Stephanie Delaune, Charlie Jacomme, Adrien Koutsos and Solène Moreau Foundations of the Squirrel meta-logic for reasoning over security protocols (abstract) PRESENTER: David Baelde

10:30-12:00 Session 37E: WST Workshop: Decidability and Analysis (WST 2021)

Chair:

Carsten Fuhs

10:30	Florian Frohn, Jürgen Giesl and Marcel Hark Polynomial Loops: Termination and Beyond (abstract)
11:00	Fabian Mitterwallner and Aart Middeldorp Polynomial Termination over N is Undecidable (abstract)
11:30	Frank Emrich, Jera Hensel and Jürgen Giesl Modular Termination Analysis of C Programs (abstract)

11:30-12:00 Session 38: Open Discussion (ARCADE 2021)

Chair:

Martin Suda

Location: ZoomRoom 1

12:00-12:30Break

12:30-14:00 Session 39A: The 10th TPTP Tea Party (CADE-28)

Location: ZoomRoom 1

12:30-14:00 Session 39B: Non-Fregean Logic Tutorial (CADE-28)

Location: ZoomRoom 4

12:30-13:30 Session 39C: LFMTP Workshop: Invited Talk (LFMTP 2021)

Chair:

Enrico Tassi

Location: ZoomRoom 3

12:30

Matthieu Sozeau

The MetaCoq Project

12:30-14:00 Session 39D: WST Workshop: Runtime Complexity (WST 2021)

Chair:

Salvador Lucas

Location: ZoomRoom 2

12:30	Fabian Meyer, Marcel Hark and Jürgen Giesl Analyzing Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes (abstract)
13:00	Thaïs Baudon, Carsten Fuhs and Laure Gonnord Parallel Complexity of Term Rewriting Systems (abstract)
13:30	Carsten Fuhs Between Derivational and Runtime Complexity (abstract)

13:30-14:00 Session 40: Foundations: MetaCoq (LFMTP 2021)

Chair:

Enrico Tassi

Location: ZoomRoom 3

13:30

Florian Rabe and Navid Roux

Translating Formalizations of Type Theories from Intrinsic to Extrinsic Style (abstract)

PRESENTER: Navid Roux

14:00-14:30Break

14:30-16:00 Session 41A: The 10th TPTP Tea Party (CADE-28)

Location: ZoomRoom 1

14:30-16:00 Session 41B: Non-Fregean Logic Tutorial (CADE-28)

Location: ZoomRoom 4

14:30-16:00 Session 41C: LFMTP Workshop: Formalization (LFMTP 2021)

Chair:

Giselle Reis

Location: ZoomRoom 3

14:30	Mary Southern and Gopalan Nadathur Adelfa: A System for Reasoning about LF Specifications (abstract) PRESENTER: Mary Southern
15:00	Bruno Cuconato, Jefferson de Barros Santos and Edward Hermann Haeusler A logical framework with a graph meta-language (abstract) PRESENTER: Bruno Cuconato
15:30	Anduo Wang Towards a Semantic Framework for Policy Exchange in the Internet (abstract)

14:30-16:30 Session 41D: WST Workshop: Term Rewriting and Termination Arguments (WST 2021)

Chair:

Jürgen Giesl

Location: ZoomRoom 2

14:30	Salvador Lucas Did Turing Care of the Halting Problem? (abstract)
15:00	Deivid Do Vale and Niels van der Weide Formalizing Higher-Order Termination in Coq (abstract)
15:30	Etienne Payet Observing Loopingness (abstract)
16:00	Amir Ben-Amram, Jesús J. Doménech and Samir Genaim Loops for which Multiphase-Linear Ranking Functions are Sufficient (abstract)