Pi Squared Papers

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.

Jun 01, 2023

We present matching µ-logic, which is a unifying logic for specifying and reasoning about programs and programming languages. Matching µ-logic uses its formulas, called patterns, to uniformly express programs’ static structures, dynamic behaviors, and logical constraints.

Jan 01, 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.

Jul 01, 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.

Aug 01, 2020

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 mu-logic, an extension of matching logic with a least fixpoint mu-binder.

Jun 01, 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.

Jun 01, 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.

Jan 01, 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.

Dec 01, 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.

Jun 01, 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%.

Jun 01, 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.

Jan 01, 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

Aug 22, 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.

Aug 01, 2010