LETOS -- A Lightweight Execution Tool for Operational Semantics A lightweight tool is proposed to aid in the development of operational semantics. To use letos, an operational semantics must be expressed in its meta-language, which itself is a superset of Miranda. The letos compiler is smaller than comparable tools, yet letos is powerful enough to support publication quality rendering using LaTeX, fast enough to provide competitive execution and tracing using Miranda or Haskell, and versatile enough to support derivation tree browsing using Netscape. Letos has been applied to a Java Secure Processor, which is a version of the Java Virtual Machine intended to run on smart cards. Letos has also been used with subsets of various programming languages. Letos is unique in that it helps to check that a specification is operationally conservative.
Keywords for this software
References in zbMATH (referenced in 8 articles )
Showing results 1 to 8 of 8.
- Cimini, Matteo; Mousavi, Mohamamdreza; Reniers, Michel A.; Gabbay, Murdoch J.: Nominal SOS (2012)
- Meseguer, José; Roşu, Grigore: The rewriting logic semantics project (2007)
- Mousavi, Mohammadreza; Reniers, Michel A.; Groote, Jan Friso: SOS formats and meta-theory: 20 years after (2007)
- Mousavi, Mohammad Reza; Reniers, Michel A.: Prototyping SOS meta-theory in Maude (2006)
- Barthe, Gilles; Courtieu, Pierre; Dufay, Guillaume; Melo de Sousa, Simão: Tool-assisted specification and verification of typed low-level languages (2005)
- Siveroni, Igor A.: Operational semantics of the Java Card Virtual Machine (2004)
- Barthe, G.; Dufay, G.; Huisman, M.; de Sousa, S.Melo: Jakarta: A toolset for reasoning about JavaCard (2001)
- Hartel, Pieter H.: LETOS - a lightweight execution tool for operational semantics. (1999)