Start / Type Theory Forall / 28 formally verifying smart contracts pruvendo

#28 Formally Verifying Smart Contracts - Pruvendo

71 min • 15 februari 2023

In this episode we host another company that does formal method in the context of the Everscale Blockchain, and Solidity smart contracts. How and why they use formal methods in this context? Who are their clients? What are the caveats?

Links

Senaste avsnitt

#52 Why is Haskell so special - Lennart Augustsson

10 juli | 91 min

#51 s/Coq/Rocq - Nicolas Tabareau

4 juni | 102 min

#50 The Expression Problem, Functional Pearls, Program Calculation - Wouter Swierstra

14 maj | 127 min

#49 Self-Education in PL - Ryan Brewer

14 mars | 144 min

#48 Bell Labs - David MacQueen

21 januari | 130 min

00:00 -00:00

#28 Formally Verifying Smart Contracts - Pruvendo

Links

Senaste avsnitt

#52 Why is Haskell so special - Lennart Augustsson

#51 s/Coq/Rocq - Nicolas Tabareau

#50 The Expression Problem, Functional Pearls, Program Calculation - Wouter Swierstra

#49 Self-Education in PL - Ryan Brewer

#48 Bell Labs - David MacQueen

#47 The History of LCF, ML and HOPE - David MacQueen

#46 Realizability, BHK, CPS Translation, Dialectica - Pierre-Marie Pédrot

#45 What is Type Theory and What Properties we Should Care About - Pierre-Marie Pédrot

#44 Theorem Prover Foundations, Lean4Lean, Metamath - Mario Carneiro

#43 PL in the Industry and Summer Schools - Patrick and Eric

#42 Distributed Systems, Microservices, and Choreographies - Fabrizio Montesi

#41 The Value of PL (and) Education - Satnam Singh

#40 Secure Voting - Joe Kiniry

#39 Equality, Quotation, Bidirectional Type Checking - David Christiansen

#38 Haskell, Lean, Idris, and the Art of Writing - David Christiansen

#37 Compilers, Staging, Futamura Projections - Guannan Wei

#36 Behind the Person Behind this Podcast - Pedro Abreu

#35 Teika, Self-Education and F***ing Floating Points - Eduardo Rafael

#34 Foundations of Theorem Provers and Cedille2 - Andrew Marmaduke

#33 Z3 and Lean, the Spiritual Journey - Leo de Moura

#32 TyDe Systems - Jan de Muijnck-Hughes

#31 Discussing Problems in PL and Academia - Jan de Muijnck-Hughes

#30 Actors, GADTs and Burnout - Dan and Pedro

#29 Can PL theory make you a better software engineer? - Jimmy Koppel

#28 Formally Verifying Smart Contracts - Pruvendo

#27 Formalizing an OS: The seL4 - Gerwin Klein

#26 Mechanizing Modern Mathematics - Kevin Buzzard

#25 Formally Verifying the Tezos Codebase - Formal Land

#24 The History of Isabelle - Lawrence Paulson

#23 What is the SIGPLAN? - Jens Palsberg and Jonathan Aldrich

#22 Impredicativity, LEM, Realizability and more - Cody Roux

#21 Denotational Design - Conal Elliott

#20 Huaweii, String Diagrams, Game Semantics - Dan R. Ghica

#19 Experience Report: Learning Coq - Patrick and Supun

#18 Gödel's Incompleteness Theorems - Cody Roux

#17 The Lost Elegance of Computation - Conal Elliott

#16 Agda, K Axiom, HoTT, Rewrite Theory - Jesper Cockx

#15 Coq Projects, Agda, Idris, Kind - Nitin and Eric

#14 POPL, Parametricity, Scala, DOT - Nitin and Eric

#13 C/C++, Emacs, Haskell, and Coq. The Journey - John Wiegley

#12 Tenure, Sexism and ADHD - Talia Ringer

#11 FP, Monads, GHC, and beyond - Alejandro Serrano

#10 Classical Logic vs Intuitionistic Logic - Thorsten Altenkirch and Anupam Das

#9 Logic and Proof Theory - Anupam Das

#8 Cedille - Chris Jenkins

#7 Hacking Isabelle's Internals - Dan Matichuk

#6 All The Dumb Questions on Gradual Types - Zeina Migeed

#5 The History of Coq'Art - Yves Bertot

#4 Theorem Provers, Functional Programming and Companies - Eric Bond

#3 ML for PL and Mental Health - Dan Zheng

#2 Grad School Life - Rajan Walia and John Sarracino

#1 What is PL research? - Prof. Ben Delaware

#0 Cool Internships in PL - Pedro Abreu