RSS Meetups are monthly gatherings of LASIGE members with research interests mainly in Software Architecture, Verification, Testing, Programming Languages, Type Systems, Logic, Concurrency, and Formal Methods.

Title: Proving theorems in Lean for mere mortals (Tutorial)
Speaker: Alcides Fonseca (LASIGE, DI/FCUL)
When: Tuesday, June 2, 15h00
​Where:  https://videoconf-colibri.zoom.us/j/98488111868

Abstract:

Do you know what the Curry-Howard isomorphism is? If your answer was no, this is the talk just for you! Even if you have never proved anything in your life, this talk is still for you!

This tutorial will have a follow-at-home format, where you may practice Lean proving really simple theorems (natural numbers, inequalities, simply-typed lambda calculus) without requiring a deep understanding of the Lean language or Dependently Typed Theory.

When our time is up, you will hopefully understand the basics of how theorems can be proved using programming languages, you will have learnt some tactics to help you in your own theorems, and you will see a path ahead to learn more about LEAN if you so wish. But let’s be realistic: it’s much easier to prove things on paper. When you make a mistake, the paper won’t point it out.

Bio:

Alcides Fonseca is an Assistant Professor at the Faculty of Sciences of the University of Lisbon. Alcides has a PhD, a MSc and a BSc from the University of Coimbra, where he also was a Visiting Lecturer. Alcides has participated in several national and international projects, such as the CMU|Portugal Aeminium, and industry projects, being a consultant for several startups (Genomed, SmashTech, Sentilant, Spero, Burocratik) and multinational companies (Ogilvy & Mather). Currently, Alcides is affiliated with the LASIGE research center, where he is the local PI of the CMU|Portugal CAMELOT project, a collaboration between Feedzai, LASIGE, IST, UC and CMU.