This is a work in progress which is quickly evolving! Stay tuned.

Rholang & RChain

Rholang is a concurrent programming language, with a focus on message-passing, formally modeled by the ρ-calculus, a reflective, higher-order extension of the π-calculus. It is designed to be used to implement protocols and "smart contracts" on a general-purpose blockchain, but could be used in other settings as well.

The open-source RChain project is building a decentralized, economically secure, censorship-resistant, public, global compute infrastructure and blockchain. It will host and execute programs popularly referred to as smart contracts. It will be trustworthy, scalable, concurrent, with proof-of-stake consensus and content delivery.

My main Rholang work is going on in /Languages/GroundedRho. This work started as an implementation of the ρ-calculus with ground terms (Bool, Int, String) and name variables. It is quickly becoming a full scale implementation of RChain Rholang.

K Framework Learning Materials

I am currently learning K Framework. I will curate all of the relevant materials that I encounter/create here.

Check out my attempt at a cheat sheet for K Framework

Resources

Getting Started

• Tutorials/Grigore Rosu on Youtube / My YouTube K Framework playlist (tutorial videos in order)

• K Overview video

• K Framework GitHub

Deeper Dive: Papers

• K - A Semantic Framework for Programming Languages and Formal Analysis Tools

• K Primer

• K Overview and SIMPLE Case Study

• Overview of the K Semantic Framework

• All-Path Reachability Logic

• Matching Logic

• A Truly Concurrent Semantics for K Framework Based on Graph Transformarions

• Abstract Semantics for K Module Composition

• A Language-Independent Approach to Smart Contract Verification

• Semantics-Based Program Verifier for all Languages

• Specifying Languages and Verifying Programs with K

• IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics