Pi Squared Papers

This paper gives an overview of the universal language semantic framework, K, that is at the core of Pi Squared's technology.  Specifically, it discusses recent innovations and optimizations that have made K's automatically generated interpreters match and even outperform existing mainstream manually-written interpreters/VMs.

February 2025

This paper gives an overview of Pi Squared's Proof of Proof approach to universal and correct-by-construction verifiable computing.

February 2025

This paper introduces Pi Squared's Universality Stack, a three-tiered architecture comprising the Universal Settlement Layer (USL), the Universal Language Machine (ULM), and the Universal Consensus Protocol (UCP).

February 2025

In this paper, we present a nominal extension to matching logic called NML that facilitates specification and reasoning about languages with binders and an alpha-structural Induction Principle for any nominal binding signature with set variables and fixpoint operators. We illustrate the use of the principle to prove properties of the 𝜆-calculus, the computation model underlying functional programming languages. The techniques generalize to other languages with binders. The proofs have been written in and generated using Metamath Zero.

January 2025

We present the syntax and the proof system of matching logic and introduce the research problem of producing succinct cryptographic proofs for checking matching logic proofs, aka Proof of Proof.

June 2023

In this 240-page PhD thesis by our CTO, we present matching µ-logic as a unifying logic for specifying and reasoning about programs and programming languages, along with various foundational findings and applications.

May 2023

We pursue the vision of an ideal language framework, where programming language designers only need to define the formal syntax and semantics of their languages, and all language tools are automatically generated by the framework.

July 2021

We propose a novel definition of binders using matching logic, where the binding behavior of object-level binders is directly inherited from the built-in exists binder of matching logic. We show that the behavior of binders in various logical systems such as lambda-calculus, System F, pi-calculus, pure type systems, can be axiomatically defined in matching logic as notations and logical theories.

August 2020

Matching logic is a logic for specifying and reasoning about structure by means of patterns and pattern matching. This paper makes two contributions. First, it proposes a sound and complete proof system for matching logic in its full generality. Previously, sound and complete deduction for matching logic was known only for particular theories providing equality and membership. Second, it proposes matching µ-logic, an extension of matching logic with a least fixpoint µ-binder.

June 2019

We present the most complete and thoroughly tested formal semantics of x86-64 to date. Our semantics faithfully formalizes all the non-deprecated, sequential user-level instructions of the x86-64 Haswell instruction set architecture.

June 2019

A developing field of interest for the distributed systems and applied cryptography communities is that of smart contracts: self-executing financial instruments that synchronize their state, often through a blockchain. One such smart contract system that has seen widespread practical adoption is Ethereum, which has grown to a market capacity of 100 billion USD and clears an excess of 500,000 daily transactions.

January 2018

This paper presents ''matching logic'', a first-order logic (FOL) variant for specifying and reasoning about structure by means of patterns and pattern matching. Its sentences, the ''patterns'', are constructed using ''variables'', ''symbols'', ''connectives'' and ''quantifiers'', but no difference is made between function and predicate symbols.

December 2017

We present a negative semantics of the C11 language---a semantics that does not just give meaning to correct programs, but also rejects undefined programs. We investigate undefined behavior in C and discuss the techniques and special considerations needed for formally specifying it.

June 2015

This paper presents KJS, the most complete and throughly tested formal semantics of JavaScript to date. Being executable, KJS has been tested against the ECMAScript 5.1 conformance test suite, and passes all 2,782 core language tests. Among the existing implementations of JavaScript, only Chrome V8's passes all the tests, and no other semantics passes more than 90%.

June 2015

This paper presents K-Java, a complete executable formal semantics of Java 1.4. K-Java was extensively tested with a test suite developed alongside the project, following the Test Driven Development methodology.

January 2015

This thesis demonstrates the ability to formalize the operational semantics of complex programming languages in the K Semantic Framework, which pro- vides an interpreter as well as analysis tools for exploring the state space of programs and performing static reasoning about programs.

August 2013

This paper gives an overview of the K framework: what it is, how it can be used, and where it has been used so far. It also proposes and discusses the K definition of Challenge, a programming language that aims to challenge and expose the limitations of existing semantic frameworks.

August 2010