Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CALCO.2019.1
URN: urn:nbn:de:0030-drops-114296
URL: https://drops.dagstuhl.de/opus/volltexte/2019/11429/
Chen, Xiaohong ; Rosu, Grigore
Matching mu-Logic: Foundation of K Framework (Invited Paper)
| pdf-format: |
|
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 mu-logic as the foundation of K and discuss some of its applications in defining constructors, transition systems, modal mu-logic and temporal logic variants, and reachability logic.
BibTeX - Entry
@InProceedings{chen_et_al:LIPIcs:2019:11429,
author = {Xiaohong Chen and Grigore Rosu},
title = {{Matching mu-Logic: Foundation of K Framework (Invited Paper)}},
booktitle = {8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)},
pages = {1:1--1:4},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-120-7},
ISSN = {1868-8969},
year = {2019},
volume = {139},
editor = {Markus Roggenbach and Ana Sokolova},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/11429},
URN = {urn:nbn:de:0030-drops-114296},
doi = {10.4230/LIPIcs.CALCO.2019.1},
annote = {Keywords: Matching mu-logic, Program verification, Reachability logic}
}
| Keywords: | Matching mu-logic, Program verification, Reachability logic | |
| Seminar: | 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019) | |
| Issue date: | 2019 | |
| Date of publication: | 25.11.2019 |
