FMSE
Formal
Methods in
Software Engineering
Events Summer School on Language Frameworks ... Anonymous  Login

SSLF12 - Summer School on Language Frameworks 2012

.: Presentations :: Workshop :: Registration & Accommodation :: Grants :: Venue :: Organizers :: Registration form :.

New Preliminary program :: List of participants :: Pictures :: Workshop program

NewSlides

Summer School

on

Language Frameworks

(Frameworkuri pentru proiectarea și analiza limbajelor de programare)

SinaiaRomania, July 23-31, 2012.


New programming languages are proposed on a regular basis, and existing languages are continuously updated and extended to handle new requirements and paradigms. In such a dynamic field, tool supported frameworks to help designers develop a programming language and experiment with it are crucial.

The summer school is centered around the presentation of six state-of-the art language frameworks. The language frameworks will be discussed at a relaxed pace, by means of tutorials, hands-on projects, and plenty of discussions in a picturesque place in the Carpathian Mountains. Additionally, the summer school features an associated workshop where participants can discuss the synergies among the different frameworks and their own ongoing work.

Language Frameworks

The summer school will include detailed presentations/tutorials of the following language frameworks (listed alphabetically).


K

Presenter: Grigore Rosu

K is a rewrite-based executable semantic framework in which programming languages, type systems, and formal analysis tools can be defined using configurations, computations, and rules:

  • Configurations organize the state into units called cells, which are labeled and can be nested.
  • Computations carry computational meaning by extending the abstract syntax of the original language with list structures sequentializing computational tasks. Computations are like any other terms in a rewriting environment: they can be matched, moved from one place to another, modified, or deleted.
  • K (rewrite) rules make explicit which parts of the term are read-only, write-only, read-write, or are not shared at all.

These features make K suitable for defining truly concurrent languages with control-intensive features such as abrupt termination, exceptions, or call/cc.


Maude

Presenter: Jose Meseguer

Maude is a high-performance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications. Rewriting logic is a logic of concurrent change that can naturally deal with state and with concurrent computations. It has good properties as a general semantic framework for giving executable semantics to a wide range of languages and models of concurrency. In particular, it supports concurrent object-oriented computation very well.

The same reasons that make rewriting logic a good semantic framework make it also a good logical framework, that is, a metalogic in which many other logics can be naturally represented and executed. Maude supports in a systematic and efficient way logical reflection. This makes Maude remarkably extensible and powerful, supports an extensible algebra of module composition operations, and allows many advanced metaprogramming and metalanguage applications.

Indeed, some of the most interesting applications of Maude are metalanguage applications, in which Maude is used to create executable environments for different logics, theorem provers, languages, and models of computation.


PLanCompS

Presenter: Peter Mosses

PLanCompS (Programming Language Components and Specifications) aims to establish and test the practicality of a component-based framework for the design, specification and implementation of programming languages.

The main novelty of the PLanCompS approach is the creation of a collection of highly reusable language components called fundamental constructs or funcons. Crucially, the semantic specification of each funcon is independent, not needing any reformulation when funcons are combined or new funcons are added to the collection; this is possible using MSOS (a modular variant of structural operational semantics).

The semantics of a programming language is specified by inductively translating each program phrase to a combination of funcons. Tools have been developed to execute the MSOS of funcons, which allows empirical validation of the specified semantics of languages and funcons.


Rascal

Presenter: Paul Klint

Rascal is a domain-specific language for meta-programming, this is the activity of writing meta-programs. Any program that takes another program or meta-data about that program --- as input, or produces it as output, or both -- is a meta-program.

Rascal supports the Extract-Analyze-Synthesize (EASY) paradigm: using Rascal you create programs that read, analyse, transform, generate and/or visualize other programs. Rascal can also be used for the implementation of Domain-Specific Languages (DSLs). The range of programs to which meta-programming can be applied is large: from programs in standard languages like Java or PHP to DSLs for describing high-level system models or applications in specialized areas like forensics, gaming or finance. Meta-data like version histories, test results or performance data are also used as input for meta-programs.

Rascal has been designed as a one-stop-shop for meta-programming and supports the complete cycle from grammar definition and parser generation to tree construction/traversal/transformation, fact extraction, semantic analysis, statistical analysis, code generation and visualization. As an extension of Eclipse/IMP, Rascal also provides IDE features like syntax highlighting, error reporting, outlining, and hyperlinking  Extensive online documentation is available at http://tutor.rascal-mpl.org/.  You can ask questions about Rascal at http://ask.rascal-mpl.org/.


Redex

Presenter: Robby Findler

PLT Redex is a domain-specific language designed for specifying and debugging operational semantics. Write down a grammar and the reduction rules, and PLT Redex allows you to interactive explore terms and to use randomized test generation to attempt to falsify properties of your semantics.

PLT Redex is embedded in Racket, meaning all of the convenience of a modern programming language is available, including standard libraries (and non-standard ones) and a program-development environment.

 


Spoofax

Presenter: Eelco VisserGuido Wachsmuth

Spoofax is a platform for developing textual domain-specific languages with full-featured Eclipse editor plugins. With the Spoofax/IMP language workbench, you can write the grammar of your language using the high-level SDF grammar formalism. Based on this grammar, basic editor services such as syntax highlighting and code folding are automatically provided. Using high-level descriptor languages, these services can be customized. More sophisticated services such as error marking and content completion can be specified using rewrite rules in the Stratego language.


Workshop

A workshop associated to the summer school will be held on July 30-31. The program of the workshop is flexible. Currently, we plan to discuss synergies between the different language frameworks. Also, the participants of the summer school can present their own ongoing work, and discuss how they think they can use what they learrned in their future research. If time allows, the participants may also be given challenges, e.g., "can you define this little language in each framework?".

Registration and Accommodation

The registration fee is 1500 LEI (the new Romanian LEU is known also as RON) (approx. 340 Euro). This includes lunch and coffee/tea for 9 days, and the banquet. The summer school will be held at the Rowa Dany Hotel. A limited number of rooms are reserved at a special rate for participants (about 40 Euro/night for single and about 25 Euro/night for sharing a double room). These rooms will be assigned based on the on a first-come, first-served basis. Please register using the registration form. The registration fee will be paid on arrival.

We intend to keep registration open until the beginning date of the school. If the number of registered participants reaches the capacity of the conference room, then the organizers will take the freedom to stop the registration process.

In order to reserve a room at the special rate, the registration should be done before July 1st.

Grants

There are a limited number of grants for excellent participants from Romania. A grant may cover the travel, accommodation, and the registration fees.

The deadline for applying for a grant is June 15. Grants applicants must provide a short CV and a motivation letter describing why they wish to attend the summer school.

Please register here.

Venue

1With its sub-alpine climate, Sinaia is characterized by an exceptionally pleasant weather all through the summer, with an average temperature of 15 degrees C. For those who enjoy mountain trips and activities in the middle of nature, Sinaia is the main gate to the Bucegi Massif with its large crest of grassy stone in an ascending line from Varful cu Dor (1885 m) to Piatra Arsa (2075m), Babele (2290m), Caraiman (2385m), Costila (2490m) and Omu (2507m).

Sinaia is excellently placed for both those who want a couple of hours’ strolls and those who enjoy strenuous full-day hikes. It accommodates all tastes, ranging from rather easy climbs to strenuous goat trails. The great vistas that you can get from many of the laterally emerging peaks of the Bucegi Plateau make it more than worthwhile. Besides, mountain rescue teams patrol the area. The quirky, powerful forces of nature have carved many a monument around the place, such as this cluster of gigantic stone mushrooms, nicknamed "Babele" (The Old Ladies), and a huge block of stone shaped like a human skull, with deep sunk orbits and mysterious smile, known as the "Sphinx".

Sinaia has a tonic, stimulating bio-climate, with very clean air, rich in oxygen, ultraviolet radiation, and negative ionization, all of which have positive effects on the human body. In Cainelui Valley there are also some mineral springs gushing forth sulfur-ferric water and other soluble minerals. Further information can be obtained from a range of websites and publications.

By plane. The closest airport is "Henri Coanda" Bucharest International (formerly Otopeni International). All major international airlines fly to/from this airport.

By car. Sinaia is located close to express road DN 1 (E 60) at 120 km distance from Bucharest, 100 km from Henri Coanda International Airport, and 60 km from Brasov. DN 1 (E 60) is an express road, with 2 lanes in each direction on most of its length and therefore good travel speeds can be reached.

By bus ("maxi-taxi"). Several companies operate bus routes to Prahova Valley via Sinaia. There are long distance lines (ex. Bucharest - Tg. Mures). The stop of the long distance lines is in the parking lot of the Railway station.

A transporter for Otopeni - Sinaia route can be found at http://www.bucharestairporttransfer.eu/airport_transfer/romania-otopeni_airport-sinaia.

You can contact the Rowa Dany Hotel for transfer from airport to Sinaia. A transfer is about 300 LEI (approx 68 Euro). They also have the posibility to transfer groups.

Organizers

Formal Methods in Software Engineering (FMSE) of the Faculty of Computer Science (Fii), Alexandru Ioan Cuza University of Iasi (UAIC)

Formal Systems Laboratory (FSL) of the Department of Computer Science at the University of Illinois at Urbana-Champaign (UIUC)

Contact us

Email:  sslf12@info.uaic.ro

Telephone: +40 232 201536

Fax: +40 232 201490

Acknowledgment

This summer school has been made possible by a grant offered by UEFISCDI Programul IDEI - Scoli de Studii Avansate.

Slides

P. Mosses - PLanCompS (pdf, zip)

J. Meseguer - The Rewriting Logic Semantics Project and its Maude Implementation (pdf)

J. Meseguer - The Rewriting Semantics of PARALLEL (pdf)

In page 10 of the presentation a case study on the PARALLEL begins; after this, the presentation continues.

P. Klint Rascal - Introduction (pdf)

P. Klint Rascal - Overview (pdf)

R. Findler - See the site Redex @ SSLF

G. Rosu K Overview (pptx)

R. Diaconescu Trekking Sinaia (pdf)

Pictures

1 2 3


1Sursa textului: http://www.marshall.edu/natoasi/transp-lodging.html

NEWS
New publication : Model checking recursive programs interacting via ... - 01 feb 2015

Almost all modern imperative programming languages include operations for dynamically manipulating the heap, for example by allocating and deallocating objects, and by updating reference fields. In the presence of recursive ... (more)


New publication : K-Java: A Complete Semantics of Java - 10 sep 2014

This paper presents K-Java, a complete executable formal semantics of Java 1.4.
K-Java was extensively tested with a test suite developed alongside the project, following the Test Driven Development methodology.
more)


New publication : K-Java: A Complete Semantics of Java - 09 jul 2014

This paper presents K-Java, a complete executable formal semantics of Java 1.4.
K-Java was extensively tested with a test suite developed alongside the project, following the Test Driven Development methodology.
more)


New publication : Engineering Hoare Logic-based Program Verification in ... - 30 oct 2013

We propose a language-independent symbolic execution framework for languages endowed with a formal operational semantics based on term rewriting. Starting from a given definition of a language, a new language ... (more)


New talk: PAS 2013 - 20 oct 2013

Dorel lucanu will give a talk at PAS 2013.

(more)

     Archive

@FMSE 2010-2011