Dear Cheerful Logicianfriends, There is yet more logic happening this week! Hooray!
Time and Date: Thursday, 14 May at 8PM (Kansas Time; GMT-5) Speaker: Talia Ringer (University of Washington) Title: Proof Transformation: The Curry-Howard of Program Transformation Abstract: Programs change quickly, and proofs of program correctness must change quickly alongside the programs whose correctness they prove. I will discuss my work on tools to automate the process of changing proofs. At the core of these tools is a set of proof transformations or strategies to transform proofs, much like program transformations inside of compilers transform programs. These proof transformations operate over proofs in a proof assistant that is based on the Calculus of Inductive Constructions, and take advantage of the wealth of information that constructive proofs contain. With them, automation can repair broken proofs, port proofs from one development to another, implement proof strategies natural to humans like "similarly," and even optimize proofs. Zoom Link: https://unimelb.zoom.us/j/846890369?pwd=TktZYmlIUGlYOU9ZaXFJcCt0TFJFZz09 Other announcements: Hannes Leitgeb's talk from last week is available at the following link if you missed it: https://ksu.zoom.us/rec/share/751nFvap6klOQ9LB0nOcR6l6Q6b8eaa80CAd_fEMykh8FQ8NnT6Q2_rLFl7f_N17 The next two week's talks are the following: Friday, 22 May at 12PM Kansas Time: Shay Logan "Hyperdoctrines and Why You Should Care About Them". Thursday 28 May at 8PM Kansas Time: Kohei Kishida (Illinois) TBA Hooray for logic! Shay -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para [email protected]. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAMTR993uSKsQaCYMs4uLWtL84xKV%3DR22sq97cR3APgMxGWyrPg%40mail.gmail.com.
