Grigore Roşu
University of Illinois, Urbana-Champaign, Illinois, USA

Matching logic is a unifying foundational logic for programming languages, specification, verification. It serves as the foundation of the K framework: a formal language framework where all programming languages must have a formal semantics and all language tools are automatically generated by the framework from the semantics at no additional costs, in a correct-by-construction manner. Matching logic also captures computation as proof. That is, any computation done with any machine following a pre-determined set of rules (a program, a processor, etc) becomes a rigorous mathematical proof of a theorem in a corresponding matching logic theory.