Formalizing Gödel’s System T in Lean

Title: Formalizing Gödel's System T in Lean Speaker: Horațiu Cheval (University of Bucharest) Abstract: In 1958, Gödel introduced his functional interpretation as a method of reducing the consistency of first-order

Unwinding of proofs

Title: Unwinding of proofs Speaker: Pedro Pinto (TU Darmstadt) Abstract: The unwinding of proofs program dates back to Kreisel in the fifties and rests on the following broad question: “What

Exponential Diophantine equations over ℚ 

Title:  Exponential Diophantine equations over ℚ Speaker: Mihai Prunescu (University of Bucharest & IMAR) Abstract: In a previous exposition we have seen that the solvability over ℚ is undecidable for

Regular matching problems for infinite trees

Title: Regular matching problems for infinite trees Speaker: Mircea Marin (West University of Timișoara) Abstract: We study the matching problem “∃σ:σ(L)⊆R?” where L and R are regular tree languages over finite ranked

Kernelization, Proof Complexity and Social Choice

Title: Kernelization, Proof Complexity and Social Choice Speaker: Gabriel Istrate (West University of Timișoara) Abstract: We display an application of the notions of kernelization and data reduction from parameterized complexity to proof