K—A semantic framework for programming languages and formal analysis

Xiaohong Chen, Grigore Roşu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We give an overview on the applications and foundations of the $$\mathbb {K}$$ language framework, a semantic framework for programming languages and formal analysis tools. $$\mathbb {K}$$ represents a 20-year effort in pursuing the ideal language framework vision, where programming languages must have formal definitions, and tools for a given language, such as parsers, interpreters, compilers, semantic-based debuggers, state-space explorers, model checkers, deductive program verifiers, etc., can be derived from just one reference formal definition of the language, which is executable, and no other semantics for the same language should be needed. The correctness of the language tools is guaranteed on a case-by-case basis by proof objects, which encode rigorous mathematical proofs as certificates for every individual task that the tools do and can be mechanically checked by third-party proof checkers.

Original languageEnglish (US)
Title of host publicationEngineering Trustworthy Software Systems - 5th International School, SETSS 2019, Tutorial Lectures
EditorsJonathan P. Bowen, Zhiming Liu, Zili Zhang
PublisherSpringer
Pages122-158
Number of pages37
ISBN (Print)9783030550882
DOIs
StatePublished - 2020
Event5th International School on Engineering Trustworthy Software Systems, SETSS 2019 - Chongqing, China
Duration: Apr 21 2019Apr 27 2019

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12154 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference5th International School on Engineering Trustworthy Software Systems, SETSS 2019
CountryChina
CityChongqing
Period4/21/194/27/19

Keywords

  • Formal semantics
  • K framework
  • Matching logic

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'K—A semantic framework for programming languages and formal analysis'. Together they form a unique fingerprint.

Cite this