Program
July 1
Session 2
10:30-11:30
Pablo Barenbaum (Invited Speaker)
Proof Terms for Higher-Order Rewriting and Their Equivalence
11:30-12:00
Miguel Pagano and Álvaro Tasistro. Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory using Simple Renaming.
12:00-12:30
Jordina Francès de Mas and Juliana Bowles. A novel EGs-based framework for propositional-formula simplification.
12:30-14:00
Lunch Time
Session 3
14:00-15:00
Brigitte Pientka (Invited Speaker)
Mechanizing Session-Types: Enforcing linearity without linearity
15:00-15:30
Alberto Momigliano and Martina Sassella. More Church-Rosser Proofs in Beluga.
15:30-16:00
Coffe Break
Session 4
16:00-16:30
Thaynara Arielly de Lima, André Luiz Galdino, Andréia B. Avelar and Mauricio Ayala-Rincón. Formalizing Factorization on Euclidean Domains and Abstract Euclidean Algorithms.
16:30-17:00
J. Tanner Slagel, Mariano Moscato, Lauren White, César Muñoz, Swee Balachandran and Aaron Dutle. Embedding Differential Dynamic Logic in PVS.
17:00-17:30
Laura P. Gamboa Guzman and Kristin Yvonne Rozier. Stalnaker's Epistemic Logic on Isabelle/HOL.
July 2
Session 2 (LSFA + LFMTP joint sessions)
10:30-11:30
Cynthia Kop (joint talk LSFA + LFMTP)
Cutting a proof into bite-sized chunks (Incrementally proving termination in higher-order term rewriting)
11:30-12:00
Johanna Schwartzentruber and Brigitte Pientka. Semi-Automation of Meta-Theoretic Proofs in Beluga. (LFMTP contributed talk)
12:00-12:30
Niccolò Veltri and Cheng-Syuan Wan. Semi-Substructural Logics with Additives.
12:30-14:00
Lunch Time