2 Search Results for "Chen, Xiaohong"

Document
DOI: 10.4230/LIPIcs.TYPES.2022.12
A Semantics of 𝕂 into Dedukti

Authors: Amélie Ledein, Valentin Blot, and Catherine Dubois

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract
𝕂 is a semantical framework for formally describing the semantics of programming languages thanks to a BNF grammar and rewriting rules on configurations. It is also an environment that offers various tools to help programming with the languages specified in the formalism. For example, it is possible to execute programs thanks to the generated interpreter, or to check their properties thanks to the provided automatic theorem prover called the KProver. 𝕂 is based on la Matching Logic, a first-order logic with an application and fixed-point operators, extended with symbols to encode equality, typing and rewriting. This specific la Matching Logic theory is called Kore. Dedukti is a logical framework having for main goal the interoperability of proofs between different formal proof tools. Several translators to Dedukti exist or are under development, in order to automatically translate formalizations written, for instance, in Coq or PVS. Dedukti is based on the λΠ-calculus modulo theory, a λ-calculus with dependent types and extended with a primitive notion of computation defined by rewriting rules. The flexibility of this logical framework allows to encode many theories ranging from first-order logic to the Calculus of Constructions. In this article, we present a paper formalization of the translation from 𝕂 into Kore, and a paper formalization and an automatic translation tool, called KaMeLo, from Kore to Dedukti in order to execute programs in Dedukti.
Cite as

Amélie Ledein, Valentin Blot, and Catherine Dubois. A Semantics of 𝕂 into Dedukti. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 12:1-12:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{ledein_et_al:LIPIcs.TYPES.2022.12,
  author =	{Ledein, Am\'{e}lie and Blot, Valentin and Dubois, Catherine},
  title =	{{A Semantics of \mathbb{K} into Dedukti}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{12:1--12:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.12},
  URN =		{urn:nbn:de:0030-drops-184557},
  doi =		{10.4230/LIPIcs.TYPES.2022.12},
  annote =	{Keywords: Programming language, Semantics, Rewriting, Logical framework, Type theory}
}
Document
Invited Paper
DOI: 10.4230/LIPIcs.CALCO.2019.1
Matching mu-Logic: Foundation of K Framework (Invited Paper)

Authors: Xiaohong Chen and Grigore Roşu

Published in: LIPIcs, Volume 139, 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019)

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.
Cite as

Xiaohong Chen and Grigore Roşu. Matching mu-Logic: Foundation of K Framework (Invited Paper). In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.CALCO.2019.1,
  author =	{Chen, Xiaohong and Ro\c{s}u, Grigore},
  title =	{{Matching mu-Logic: Foundation of K Framework}},
  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 =	{Roggenbach, Markus and Sokolova, Ana},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2019.1},
  URN =		{urn:nbn:de:0030-drops-114296},
  doi =		{10.4230/LIPIcs.CALCO.2019.1},
  annote =	{Keywords: Matching mu-logic, Program verification, Reachability logic}
}
  • Refine by Author
  • 1 Blot, Valentin
  • 1 Chen, Xiaohong
  • 1 Dubois, Catherine
  • 1 Ledein, Amélie
  • 1 Roşu, Grigore

  • Refine by Classification
  • 1 Theory of computation → Logic
  • 1 Theory of computation → Operational semantics

  • Refine by Keyword
  • 1 Logical framework
  • 1 Matching mu-logic
  • 1 Program verification
  • 1 Programming language
  • 1 Reachability logic
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2019
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact