56 subscribers
با برنامه Player FM !
پادکست هایی که ارزش شنیدن دارند
حمایت شده


Grigore Rosu: The K Framework – A Framework to Formally Define All Programming Languages
Manage episode 232838342 series 1652309
In the past few years, we witnessed the development of multiple smart contract languages – Solidity, Viper, Michelson, Scilla etc. These languages need to enable developers to write correct, predictable behavior smart contract code. Each language development effort therefore ends up spending resources into building formal verification toolsets, compilers, debuggers and other developer tools.
In this episode, we are joined by Grigore Rosu, Professor of computer science at UIUC (University of Illinois at Urbana-Champaign) for a deep dive into the K framework. The K framework is mathematic logic and language that enables language developers to formally define all programming languages; such as C, Solidity and JavaScript. Once a language is formally specified in the K framework, the framework automatically outputs a range of formal verification toolsets, compilers, debuggers and other developer tools for it. Updates to the language can be made directly in K. This technology has massive implications for smart contract programming language development, and formal verification efforts in the blockchain space.
We also cover his efforts to express the Ethereum virtual machine using the K framework, and to develop a new virtual machine technology, called IELE, specifically tailored to the blockchain space. Check out the episode to understand a game changing technology in the formal verification and smart contract safety space.
Topics covered in this episode:
- Grigore’s background with NASA and work on formally verified correct software
- Motivations to develop K framework
- Basic principles behind the operation of K framework
- How K deals with undefined behavior / ambiguities in a language definition
- The intersection of K framework and smart contract technology
- Runtime Verification’s collaboration with Cardano
- KEVM and IELE, smart contract virtual machines developed by Runtime Verification
- Broader implications of the K framework for the blockchain industry
Episode links:
- Defining the undefinedness of C - formalisation of C using the K framework
- IELE - a new virtual machine for the blockchain
- Runtime verification - Grigore's company
- K Semantics of the Ethereum Virtual Machine
- Short video on Grigore's partnership with Cardano
- An overview of the K framework by Runtime Verification
- A detailed technical overview of the K semantic framework
This episode is hosted by Meher Roy and Sunny Aggarwal. Show notes and listening options: epicenter.tv/239
612 قسمت
Grigore Rosu: The K Framework – A Framework to Formally Define All Programming Languages
Epicenter - Learn about Crypto, Blockchain, Ethereum, Bitcoin and Distributed Technologies
Manage episode 232838342 series 1652309
In the past few years, we witnessed the development of multiple smart contract languages – Solidity, Viper, Michelson, Scilla etc. These languages need to enable developers to write correct, predictable behavior smart contract code. Each language development effort therefore ends up spending resources into building formal verification toolsets, compilers, debuggers and other developer tools.
In this episode, we are joined by Grigore Rosu, Professor of computer science at UIUC (University of Illinois at Urbana-Champaign) for a deep dive into the K framework. The K framework is mathematic logic and language that enables language developers to formally define all programming languages; such as C, Solidity and JavaScript. Once a language is formally specified in the K framework, the framework automatically outputs a range of formal verification toolsets, compilers, debuggers and other developer tools for it. Updates to the language can be made directly in K. This technology has massive implications for smart contract programming language development, and formal verification efforts in the blockchain space.
We also cover his efforts to express the Ethereum virtual machine using the K framework, and to develop a new virtual machine technology, called IELE, specifically tailored to the blockchain space. Check out the episode to understand a game changing technology in the formal verification and smart contract safety space.
Topics covered in this episode:
- Grigore’s background with NASA and work on formally verified correct software
- Motivations to develop K framework
- Basic principles behind the operation of K framework
- How K deals with undefined behavior / ambiguities in a language definition
- The intersection of K framework and smart contract technology
- Runtime Verification’s collaboration with Cardano
- KEVM and IELE, smart contract virtual machines developed by Runtime Verification
- Broader implications of the K framework for the blockchain industry
Episode links:
- Defining the undefinedness of C - formalisation of C using the K framework
- IELE - a new virtual machine for the blockchain
- Runtime verification - Grigore's company
- K Semantics of the Ethereum Virtual Machine
- Short video on Grigore's partnership with Cardano
- An overview of the K framework by Runtime Verification
- A detailed technical overview of the K semantic framework
This episode is hosted by Meher Roy and Sunny Aggarwal. Show notes and listening options: epicenter.tv/239
612 قسمت
همه قسمت ها
×
1 Stripe: The Stablecoin (R)Evolution - John Egan 1:05:36

1 t1 Protocol: Unifying Ethereum's L2 Liquidity Through Real-Time Proving - Can Kisagun 1:01:41

1 DappCon 25: The Ticker Is $ETH - Jerome de Tychey, Joshua Dávila & Nixorokish 1:12:32

1 Lombard: Unlocking Bitcoin DeFi Through Liquid, Yield-Bearing LBTC - Jacob Phillips 1:11:09

1 ETHPrague: ETH Renaissance - Austin Griffith, Brenda Loya, Joseph Schweitzer, Marek Olszewski 1:00:25

1 Initia: Incentively Aligned Appchains - Ezaan Mangalji, Anil Lulla & Jose Maria Macedo 1:02:08

1 Ethereum Foundation: Humanity’s Shared World Computer - Hsiao-Wei Wang & Tomasz Stańczak 1:10:21

1 Taiko: Scaling Ethereum in a Decentralised Manner - Joaquin Mendes 1:08:05

1 Mysten Labs: How Sui Leverages Move to Build the Composable Web3nternet - Adeniyi Abiodun 1:03:09

1 Tally: The Software Layer for Tokenized Organizations - Dennison Bertram 1:01:21

1 Lido V3: Ushering in Institutional Staking Through stVaults - Hasu 1:19:32


1 Solana: From On-Chain Nasdaq to the Pump Fun Craze - Anatoly Yakovenko 1:18:28

1 Build on Bitcoin: Combining Bitcoin's Security With Ethereum's Versatility - Alexei Zamyatin 1:10:10

1 Puja Ohlhaver: Why Community Currencies Are Crucial for Governance in DeSoc 1:04:42

1 Nevermined: Payment System for the AI Agentic Economy - Don Gossen 1:04:38

1 Turtle Club: Helping Web3 Users Monetize Their On-Chain Activity - Esfandiar Lagevardi 1:09:25


1 Balancer: Custom AMMs and Liquidity Solutions - Fernando Martinelli 1:04:35



1 RedStone: The Oracle Pioneering the Future of DeFi - Marcin Kaźmierczak 1:04:40

1 Privado ID & Quark ID: On-Chain ZK-Powered Unified ID - Diego Fernandez & Evin McMullen 1:06:49

1 Abundance: The First 1 Gigagas/second Stack for Sovereign Rollups - Hilmar Orth 1:09:00

1 Monad: The EVM-Compatible 10,000 TPS L1 Blockchain - Keone Hon 1:10:54
به Player FM خوش آمدید!
Player FM در سراسر وب را برای یافتن پادکست های با کیفیت اسکن می کند تا همین الان لذت ببرید. این بهترین برنامه ی پادکست است که در اندروید، آیفون و وب کار می کند. ثبت نام کنید تا اشتراک های شما در بین دستگاه های مختلف همگام سازی شود.