Re: [Logica-l] Supergroup Talk This Week
https://ksu.zoom.us/j/96235058883?pwd=V0FEUWlEOG5tUUJCcnBGZGJJcnJOdz09 On Fri, May 22, 2020 at 2:11 PM Eduardo Ochs wrote: > > 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 > > > On Mon, 11 May 2020 at 23:05, Shay Logan wrote: > > > > 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ê 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+unsubscr...@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. > > -- > 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+unsubscr...@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/ -- 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+unsubscr...@dimap.ufrn.br. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAO6j_LhRxDU%2Ba%3DQJ97RAXeaw9PKdfCooG2aYAbQdnKq7nhR-1Q%40mail.gmail.com.
Re: [Logica-l] Supergroup Talk This Week
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 On Mon, 11 May 2020 at 23:05, Shay Logan wrote: > > 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ê 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+unsubscr...@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. -- 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+unsubscr...@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.
[Logica-l] Supergroup Talk This Week
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 logica-l+unsubscr...@dimap.ufrn.br. 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.
