Rewriting Logic Semantics
From FSL
Rewriting logic can be used to create executable definitions of programming languages, yielding interpreters for the defined languages which run programs directly in the language semantics. This also yields definitions of languages that can be used for formal reasoning about language properties. Examples include model checking, state-space exploration for programs with potentially unbounded state spaces, theorem proving, partial correctness via Hoare logics, and type safety/type checking.
Contents |
[edit] Definitions of Existing Languages
We have defined several existing languages using rewriting logic. These definitions can be used to both run programs in the defined language and reason about the language, and have been used in a number of contexts.
- Lambda Calculus, a commonly-used language calculus which has served as a model for many functional languages
- Beta, a statically-typed object-oriented programming language derived from Simula 67, where the unifying concept of pattern has replaced classes and methods
- Java, a statically-typed, class-based object-oriented programming language
- Prolog, a logic programming language (only partially defined)
- Scheme, a very faithful semantics of Scheme, a functional language with strong reflection and meta-programming capabilities.
[edit] Definitions of Sample Languages
We have also defined a number of research languages using rewriting logic. These have value both as examples of specific paradigms of languages (functional, imperative, object-oriented) and as basis languages which we can use in our research.
- SILF, a Simple Imperative Language with Functions, used for illustrating our framework
- CSILF, a Concurrent version of SILF, used to illustrate the addition of simple concurrency features and verification of concurrent programs
- KOOL, a dynamically typed object-oriented language
[edit] Annotated Bibliography
This bibliography provides a set of related readings for those interested in rewriting logic semantics and our approach to defining executable semantics for languages. Click Rewriting Logic Semantics Readings for more information.
[edit] Publications
- Runtime Verification of C Memory Safety
- Grigore Rosu, Wolfram Schulte and Traian Florin Serbanuta
RV'09, LNCS 5779, pp 132-151. 2009
PDF, RV slides, RV'09, LNCS, BIB - A Rewriting Logic Approach to Static Checking of Units of Measurement in C
- Mark Hills, Feng Chen and Grigore Rosu
RULE'08, ENTCS, to appear, 2008
PDF, RULE'08 slides, RULE'08, BIB - Memory Representations in Rewriting Logic Semantics Definitions
- Mark Hills WRLA'08, ENTCS, to appear, 2008
PDF, WRLA'08 slides, WRLA'08, BIB - A K Definition of Scheme
- Patrick Meredith, Mark Hills and Grigore Rosu
Technical Report UIUCDCS-R-2007-2907, October 2007
PDF, TR@UIUC, BIB - An Executable Rewriting Logic Semantics of K-Scheme
- Patrick Meredith, Mark Hills and Grigore Rosu
8th Workshop on Scheme and Functional Programming, Technical Report DIUL-RT-0701, pp. 91-103, September 2007
PDF, SCHEME'07, BIB - A Rewriting Approach to the Design and Evolution of Object-Oriented Languages
- Mark Hills and Grigore Rosu
Technical Report Bericht-Nr. 2007-7, pp. 23-26, July 2007
PDF, ECOOP'07 Doctoral Symposium slides, ECOOP'07 Doctoral Symposium, BIB - A Rewriting Logic Approach to Operational Semantics -- Extended Abstract
- Traian Florin Serbanuta, Grigore Rosu and Jose Meseguer
SOS'07, ENTCS 192(1), pp 125-141. 2007
PDF, SOS'07 Slides, ENTCS, SOS'07, BIB - KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis
- Mark Hills and Grigore Rosu
RTA'07, LNCS 4533, pp 246-256. 2007
PDF, RTA'07 slides, LNCS, RTA'07, BIB - On Formal Analysis of OO Languages using Rewriting Logic: Designing for Performance
- Mark Hills and Grigore Rosu
FMOODS'07, LNCS 4468, pp 107-121. 2007
PDF, FMOODS'07 slides, LNCS, FMOODS'07, BIB - The Rewriting Logic Semantics Project
- Jose Meseguer and Grigore Rosu J. of TCS, Volume 373(3), pp 213-237. 2007
PDF, J.TCS, BIB - A Rewrite Framework for Language Definitions and for Generation of Efficient Interpreters
- Mark Hills, Traian Florin Serbanuta and Grigore Rosu
WRLA'06, ENTCS 176(4), pp. 215-231. 2007
PDF, Experiments, ENTCS, WRLA'06, BIB - K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation
- Grigore Rosu
Technical report UIUCDCS-R-2006-2802, December 2006
PDF, TR@UIUC, BIB - A Rewriting Based Approach to OO Language Prototyping and Design
- Mark Hills and Grigore Rosu
Technical Report UIUCDCS-R-2006-2786, October 2006
PDF, TR@UIUC, BIB - KOOL: A K-based Object-Oriented Language
- Mark Hills and Grigore Rosu
Technical Report UIUCDCS-R-2006-2779, October 2006
PDF, TR@UIUC, BIB - Haskell-RL: An Equational Specification of Haskell in Maude
- Andrew Bennett
MS CS Thesis Submission
PDF, semantics - A Rewrite Logic Approach to Semantic Definition, Design and Analysis of Object-Oriented Languages
- Feng Chen, Mark Hills and Grigore Rosu
Technical Report UIUCDCS-R-2006-2702, March 2006
PDF, TR@UIUC, BIB - K: a Rewrite-based Framework for Modular Language Design, Semantics, Analysis and Implementation
- Grigore Rosu
Technical Report UIUCDCS-R-2005-2672, December 2005
PDF, Experiments, BIB - An Executable Semantic Definition of the Beta Language using Rewriting Logic
- Mark Hills, T. Baris Aktemur and Grigore Rosu
Technical Report UIUCDCS-R-2005-2650, November 2005
PDF, TR@UIUC, BIB - The Rewriting Logic Semantics Project
- Jose Meseguer and Grigore Rosu
SOS'05, ENTCS 156, pp. 27-56. 2006
PDF, SOS'05, BIB - Formal Analysis of Java Programs in JavaFAN
- Azadeh Farzan, Feng Chen, Jose Meseguer and Grigore Rosu
CAV'04, LNCS 3114, pp 501 - 505. 2004.
PDF, LNCS, CAV'04, DBLP, BIB - CS322 - Programming Language Design: Lecture Notes
- Grigore Rosu
Technical Report UIUCDCS-R-2003-2897, December 2003
PDF, TR @ UIUC, BIB - Hidden Logic
- Grigore Rosu
PhD Thesis, University of California at San Diego
PDF, Thesis@UCSD, BIB
[edit] Other Presentations
Current progress, as of April 2006, presented at
MSPLS Spring 2006 
.
