PLT Redex

Instalacja

Dokumentacja

Książka Semantics Engineering with PLT Redex (Matthias Felleisen, Robby Findler, Matthew Flatt) zawiera pełne wprowadzenie do semantyk redukcyjnych, obszerny opis Redeksa oraz przykłady zastosowań. Została wydana w 2009 roku, ale nie miałem problemów z kompatybilnością kodu z książki z bieżącą wersją środowiska. Najciekawszą nowością wydaje mi się możliwość definiowania sądów (ang. judgment), które Redex potrafi traktować w sposób algorytmiczny (tzn. automatycznie szukać wyprowadzeń) -- można w ten sposób kodować np. systemy typów oraz semantyki operacyjne (zarówno dużych jak i małych kroków). Strona książki zawiera sporo informacji.

Dokumentacja Racketa w kontekście Redeksa posiada tutorial, w którym modeluje się przykładowy język programowania, oraz szczegółową referencję do wszystkich konstrukcji biblioteki. Dokumentację można pobrać także jako 100 stronicowy plik PDF.

Artykuły

Według moich poszukiwań istnieją 4 opublikowane artykuły naukowe na temat Redeksa:

1. A Visual Environment for Developing Context-Sensitive Term Rewriting Systems, 2004, Jacob Matthews, Robert Bruce Findler, Matthew Flatt, Matthias Felleisen
2. Randomized Testing in PLT Redex, 2009 Scheme Workshop, Casey Klein, Robert Bruce Findler
3. A semantics for context-sensitive reduction semantics, 2011 APLAS, Casey Klein, Jay McCarthy, Steven Jaconette, Robert Bruce Findler
4. Run Your Research: On the Effectiveness of Lightweight Mechanization, 2012 POPL, Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, Robert Bruce Findler

Pierwszy artykuł opisuje niekompatybilną wersję narzędzia, ale zawiera wprowadzenie i referencje do tematu semantyk redukcyjnych oraz prezentuje motywacje stojące za Redeksem. Na przykładach analizowany jest język funkcyjny ze stanem, warto zobaczyć jak modeluje się go za pomocą sem. redukcyjnej. Wspomniane jest także, że PLT Redex został przez autorów użyty jako narzędzie pomocnicze do kursu o semantyce.

Drugi artykuł prezentuje korzyści z modelowania języków programowania w Redeksie poprzez pokazanie jak testowanie losowe pomaga odnaleźć błędy w modelach. Następnie opisane jest jak znaleziono błędy w specyfikacji R6RS języka Scheme. Na koniec naszkicowano w jaki sposób działa generator losowy używany przez funkcję redex-check.

Trzeci artykuł opisuje jakie konteksty można wyrazić w Redeksie oraz formalizuje w jaki sposób można zapisać (w sposób generyczny) dekompozycję relacyjnie oraz algorytmicznie.

Czwarty artykuł najpierw pokazuje jak pracuje się w PLT Redeksie (na przykładzie języka zawierającego call/cc), a następnie prezentuje wyniki analizy modeli Redeksowych do 9 artykułów z konferencji ICFP 2009.