Theory of Computation

Session coordinator: Mauricio Ayala-Rincón

Zoom link https://us02web.zoom.us/j/82214315115?pwd=VGFBa0dFWTFUY0UxK08waGRjb0dXQT09

Time Zone: GMT - 3


Plenary Speaker

Nao Hirokawa (Japan Advanced Institute of Science and Technology, Japan)


Session Speakers:


Christopher Lynch (Clarkson University, USA)


Adam D. Barwell (Imperial College London, England)


Manfred Schmidt-Schauss (Goethe University of Frankfurt, Germany)


Haniel Barbosa (Universidade Federal de Minas Gerais, Brazil)


Thaynara Arielly de Lima (Universidade Federal de Goias, Brazil)


Mauricio Ayala-Rincón (Universidade de Brasília, Brazil)



Book of Abstracts



Session Schedule

Tuesday, January 18, 2022

Invited Tutorial Part 1: Thaynara Arielly de Lima and Mauricio Ayala-Rincón

Title: Formalizing Theorems with PVS

Time: 8:00 am - 10:30 am


Invited Tutorial Part 2: Thaynara Arielly de Lima and Mauricio Ayala-Rincón

Title: Formalizing Theorems with PVS

Time: 15:10 am - 17:10 pm


Wednesday, January 19, 2022

Invited talk: Manfred Schmidt-Schauss

Title: Nominal unification and extensions for applications in higher order languages

Time: 10:30 am - 11:30 am


Conributed Talk: Daniella Santaguida

Title: Nominal Commutative Narrowing

Time: 11:40 am - 12:20 pm


Contributed Talk: Ali Khan Caires Ribeiro Santos

Title: A nominal semantics for first-order logic

Time: 12:20 am - 13:00 pm


Invited Talk: Christopher Lynch

Title: Equational Reasoning, Unification and Applications

Time: 15:10 pm - 16:10 pm


Contributed Talk: Gabriela de Souza Ferreira

Title: Anti-Unification for syntactic, commutative and associative theories

Time: 16:10 pm - 16:50 pm


Contributed Talk: Andrés Felipe González Barragán

Title: Modular Anti-Unification

Time: 16:50 pm - 17:30 pm


Contributed Talk: Gabriel Ferreira Silva

Title: Formalising AC-unification

Time: 17:30 pm - 18:10 pm


Thursday, January 20, 2022

Invited Tutorial Part 3: Thaynara Arielly de Lima and Mauricio Ayala-Rincón

Title: Formalizing Theorems with PVS

Time: 10:30 am - 12:30 am


Invited Talk: Haniel Barbosa

Title: Better SMT proofs for certifying compliance and correctness

Time: 15:10 pm - 16:10 pm


Contributed talk: Thiago Mendonça Ferreira Ramos

Title: Formalization of the Undecidability of the Post Correspondence Problem

Time: 16:10 pm - 16:50 pm


Contributed talk: Fabrício Sanchez

Title: Towards a Formalization of Nominal Sets in Coq

Time: 16:50 pm - 17:30 pm


Contributed talk: Nikson Ferreira

Title: A rounding error analysis exercise with the PRECiSA tool in PVS

Time: 17:30 pm - 18:10 pm


Friday, January 21, 2022

Invited Talk: Adam D. Barwell

Title: An Introduction to Process Calculi, Session Types and Handling Crash-Stop Failures

Time: 8:30 am - 9:30 am


Contributed Talk: Daniel Saad Nogueira Nunes

Title: Grammar Compression By Induced Suffix Sorting

Time: 9:40 am - 10:20 am