Episódio 41: Lean e Verificação de Software, com Leonardo de Moura (AWS)

[Adolfo Neto]

Neste episódio do Fronteiras da Engenharia de Software, Adolfo Neto entrevista o pesquisador Leonardo de Moura, Senior Principal Applied Scientist no Grupo de Raciocínio Automatizado na AWS e Chief Architect da Lean FRO. Leonardo é reconhecido por diversas contribuições, entre elas o desenvolvimento do Z3, um SMT Solver, e da Lean, que é ao mesmo tempo uma linguagem de programação funcional e um provador de teoremas.

https://fronteirases.github.io/episodios/paginas/41

--

==================================================================
Adolfo Neto

Associate Professor - Federal University of Technology, Paraná

Web: http://www.dainf.ct.utfpr.edu.br/~adolfo
Mestrado em Computação Aplicada: http://www.ppgca.ct.utfpr.edu.br
==================================================================

[Joao Marcos]

E por falar em Lean, os interessados em matemática formalizada
provavelmente irão querer ficar de olho neste projeto recente do
Terence Tao (com Tim Gowers, Ben Green, Freddie Manners):
https://terrytao.wordpress.com/2023/11/13/on-a-conjecture-of-marton/
https://mathstodon.xyz/@tao/111404473592619929
https://teorth.github.io/pfr/blueprint/dep_graph_document.html

[]s, JM

> --
> LOGICA-L
> Lista acadêmica brasileira dos profissionais e estudantes da área de Lógica <logi...@dimap.ufrn.br>
> ---
> 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 acessar essa discussão na Web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CANspyYUguAdej_2KY66CAD3-ON7op2SpUZiw7Mudn5i3d0vNrw%40mail.gmail.com.



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

[Joao Marcos]

Menos de um mês depois, a tarefa de formalização em Lean já foi concluída:
https://twitter.com/AlexKontorovich/status/1731692984771428633

JM

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