Supergroup Talk This Week

[Shay Logan]

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

[Eduardo Ochs]

Alguem sabe como fazer pra assistir a palestra de hoje?
Tou tentando descobrir ha' um tempao e o maximo que eu consegui ate'
agora foi adicionar uma referencia `a palestra no meu Google
Calendar...
[[]] =/,
Eduardo

> --
> Você recebeu essa mensagem porque está inscrito 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 logica-l+u...@dimap.ufrn.br.
> Para ver essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAMTR993uSKsQaCYMs4uLWtL84xKV%3DR22sq97cR3APgMxGWyrPg%40mail.gmail.com.

[Joao Marcos]

https://ksu.zoom.us/j/96235058883?pwd=V0FEUWlEOG5tUUJCcnBGZGJJcnJOdz09

> --
> 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 logica-l+u...@dimap.ufrn.br.

> Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CADs%2B%2B6jfbDFkhNt0EBaGyLxBX5MAF%3DBcuw7PzSwXq6v7uU_JoA%40mail.gmail.com.



--
http://sequiturquodlibet.googlepages.com/