Semantics engineering with PLT Redex

MaRDI QIDQ3655271zbMATH OpenFDO

Authors Matthias Felleisen, Bruce Findler, Matthew Flatt

Publication date 7 January 2010

zbMATH Keywords

reduction semanticssemantic models of programming languages

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Semantics in the theory of computing (68Q55)

Recommendations

• An operational semantics for Scheme
• Lem: reusable engineering of real-world semantics
• Modular rewriting semantics in practice
• Ott: Effective tool support for the working semanticist
• Ott, effective tool support for the working semanticist

Cited in

(29)

• Executable component-based semantics
• System description: lang-n-change -- a tool for transforming languages
• From specification to testing: semantics engineering for Lua 5.2
• A lazy desugaring system for evaluating programs with sugars
• Lem: reusable engineering of real-world semantics
• Macros that work together
• APLicative Programming with Naperian Functors
• MikiBeta : A General GUI Library for Visualizing Proof Trees
• Lazy tree splitting
• Systematic abstraction of abstract machines
• A calculus for language transformations
• αCheck: A mechanized metatheory model checker
• Fair enumeration combinators
• Deriving an abstract machine for strong call by need
• scientific article; zbMATH DE number 7204429 (Why is no real title available?)
• On graph rewriting, reduction, and evaluation in the presence of cycles
• Efficiency of lambda-encodings in total type theory
• Automating the functional correspondence between higher-order evaluators and abstract machines
• Towards substructural property-based testing
• Redex2Coq: towards a theory of decidability of Redex's reduction semantics
• Optimizing a non-deterministic abstract machine with environments
• An open challenge problem repository for systems supporting binders
• Cartesian reachability logic: a language-parametric logic for verifying k-safety properties
• Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space
• \( \mathbb{K}\) definitions as matching logic theories, formally
• An imperative pure calculus
• Implementing type systems for the IDE with Xsemantics
• A correspondence between type checking via reduction and type checking via evaluation
• A content semantics for quantified relevant logics. II

Describes a project that uses

Uses Software

• PLT Redex

This page was built for publication: Semantics engineering with PLT Redex

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3655271)