Matching µ-logic: Foundation of K framework

Xiaohong Chen, Grigore Roşu

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

Abstract

K framework is an effort in realizing the ideal language framework where programming languages must have formal semantics and all languages tools are automatically generated from the formal semantics in a correct-by-construction manner at no additional costs. In this extended abstract, we present matching µ-logic as the foundation of K and discuss some of its applications in defining constructors, transition systems, modal µ-logic and temporal logic variants, and reachability logic.

Original languageEnglish (US)
Title of host publication8th Conference on Algebra and Coalgebra in Computer Science, CALCO 2019
EditorsMarkus Roggenbach, Ana Sokolova
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959771207
DOIs
StatePublished - Nov 2019
Event8th Conference on Algebra and Coalgebra in Computer Science, CALCO 2019 - London, United Kingdom
Duration: Jun 3 2019Jun 6 2019

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume139
ISSN (Print)1868-8969

Conference

Conference8th Conference on Algebra and Coalgebra in Computer Science, CALCO 2019
CountryUnited Kingdom
CityLondon
Period6/3/196/6/19

Keywords

  • Matching µ-logic
  • Program verification
  • Reachability logic

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'Matching µ-logic: Foundation of K framework'. Together they form a unique fingerprint.

Cite this