#7 Hacking Isabelle's Internals - Dan Matichuk

Type Theory Forall

Контент предоставлен Pedro Abreu. Весь контент подкастов, включая эпизоды, графику и описания подкастов, загружается и предоставляется непосредственно компанией Pedro Abreu или ее партнером по платформе подкастов. Если вы считаете, что кто-то использует вашу работу, защищенную авторским правом, без вашего разрешения, вы можете выполнить процедуру, описанную здесь https://ru.player.fm/legal.

3+ y ago 1:20:52

MP3•Главная эпизода

In this episode we dive into Isabelle, the interactive theorem prover based on Higher Order Logic directly from someone who spent quite some time hacking on its internals.

Me and Daniel also talk about Mizar, Isar, the seL4, and how it is formalized.

Torwards the end of the episode we also talk a little about his current work on the binary analysis of Aarch32 Arm Archtecture at Galois.

82 эпизодов

#Science #Tech #Pedro Abreu #Type Theory #Academia #Programming Language