Symbolic Computation in Maude: Some Tapas

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

Abstract

Programming in Maude is executable mathematical modeling. Your mathematical model is the code you execute. Both deterministic systems, specified equationally as so-called functional modules and concurrent ones, specified in rewriting logic as system modules, are mathematically modeled and programmed this way. But rewriting logic is also a logical framework in which many different logics can be naturally represented. And one would like not only to execute these models, but to reason about them at a high level. For this, symbolic methods that can automate much of the reasoning are crucial. Many of them are actually supported by Maude itself or by some of its tools. These methods are very general: they apply not just to Maude, but to many other logics, languages and tools. This paper presents some tapas about these Maude-based symbolic methods in an informal way to make it easy for many other people to learn about, and benefit from, them.

Original languageEnglish (US)
Title of host publicationLogic-Based Program Synthesis and Transformation - 30th International Symposium, LOPSTR 2020, Proceedings
EditorsMaribel Fernández
PublisherSpringer
Pages3-36
Number of pages34
ISBN (Print)9783030684457
DOIs
StatePublished - 2021
Externally publishedYes
Event30th International Conference on Logic-Based Program Synthesis and Transformation, LOPSTR 2020 - Bologna, Italy
Duration: Sep 7 2020Sep 9 2020

Publication series

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

Conference

Conference30th International Conference on Logic-Based Program Synthesis and Transformation, LOPSTR 2020
Country/TerritoryItaly
CityBologna
Period9/7/209/9/20

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Symbolic Computation in Maude: Some Tapas'. Together they form a unique fingerprint.

Cite this