This text is the first comprehensive presentation of reduction semantics in one volume; it also introduces the first reliable and easy-to-use tool set for such forms of semantics. Software engineers have long known that automatic tool support is critical for rapid prototyping and modeling, and this book is addressed to the working semantics engineer (graduate student or professional language designer). The book comes with a prototyping tool suite to develop, explore, test, debug, and publish semantic models of programming languages. With PLT Redex, semanticists can formulate models as grammars and reduction models on their computers with the ease of paper and pencil. The text first presents a framework for the formulation of language models, focusing on equational calculi and abstract machines, then introduces PLT Redex, a suite of software tools for expressing these models as PLT Redex models. Finally, experts describe a range of models formulated in Redex. PLT Redex comes with the PLT Scheme implementation, available free at http://www.plt-scheme.org/. Readers can download the software and experiment with Redex as they work their way through the book. For more information (including the preface, a sample syllabus, and a quick introduction to Redex), see the Redex website at http://redex.plt-scheme.org/. Matthias Felleisen, Robert Bruce Findler, and Matthew Flatt are the authors (with Shiram Krishnamurthi) of How to Design Programs: An Introduction to Programming and Computing, also published by the MIT Press.
Cited By
- Moy C, Dimoulas C and Felleisen M (2024). Effectful Software Contracts, Proceedings of the ACM on Programming Languages, 8:POPL, (2639-2666), Online publication date: 5-Jan-2024.
- Geller A, Frank J and Bowman W (2024). Indexed Types for a Statically Safe WebAssembly, Proceedings of the ACM on Programming Languages, 8:POPL, (2395-2424), Online publication date: 5-Jan-2024.
- Hatch W, Darragh P, Porncharoenwase S, Watson G and Eide E Generating Conforming Programs with Xsmith Proceedings of the 22nd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, (86-99)
- Renaux T, Van den Vonder S and De Meuter W (2023). Secure RDTs: Enforcing Access Control Policies for Offline Available JSON Data, Proceedings of the ACM on Programming Languages, 7:OOPSLA2, (146-172), Online publication date: 16-Oct-2023.
- Sieczkowski F, Pyzik M and Biernacki D (2023). A General Fine-Grained Reduction Theory for Effect Handlers, Proceedings of the ACM on Programming Languages, 7:ICFP, (511-540), Online publication date: 30-Aug-2023.
- Augustsson L, Breitner J, Claessen K, Jhala R, Peyton Jones S, Shivers O, Steele Jr. G and Sweeney T (2023). The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming, Proceedings of the ACM on Programming Languages, 7:ICFP, (417-447), Online publication date: 30-Aug-2023.
- Amin N, Burnham J, Garillot F, Gennaro R, Künzang C, Rogozin D and Wong C (2023). LURK: Lambda, the Ultimate Recursive Knowledge (Experience Report), Proceedings of the ACM on Programming Languages, 7:ICFP, (259-274), Online publication date: 30-Aug-2023.
- Soldevila M, Ziliani B and Silvestre B (2022). From Specification to Testing: Semantics Engineering for Lua 5.2, Journal of Automated Reasoning, 66:4, (905-952), Online publication date: 1-Nov-2022.
- Koppel J, Kearl J and Solar-Lezama A (2022). Automatically deriving control-flow graph generators from operational semantics, Proceedings of the ACM on Programming Languages, 6:ICFP, (742-771), Online publication date: 29-Aug-2022.
- Greenman B Deep and shallow types for gradual languages Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, (580-593)
- Busi M, Degano P and Galletta L Towards effective preservation of robust safety properties Proceedings of the 37th ACM/SIGAPP Symposium on Applied Computing, (1674-1683)
- Henz M, Tan T, Chua Z, Jung P, Tan Y, Zhang X and Zhao J A stepper for a functional JavaScript sublanguage Proceedings of the 2021 ACM SIGPLAN International Symposium on SPLASH-E, (71-81)
- Mantovani M and Momigliano A Towards Substructural Property-Based Testing Logic-Based Program Synthesis and Transformation, (92-112)
- Buszka M and Biernacki D Automating the Functional Correspondence Between Higher-Order Evaluators and Abstract Machines Logic-Based Program Synthesis and Transformation, (38-59)
- Cimini M A Calculus for Multi-language Operational Semantics Software Verification, (25-42)
- Salis V, Sotiropoulos T, Louridas P, Spinellis D and Mitropoulos D PyCG Proceedings of the 43rd International Conference on Software Engineering, (1646-1657)
- Swalens J, Koster J and Meuter W (2021). Chocola, ACM Transactions on Programming Languages and Systems, 42:4, (1-56), Online publication date: 31-Dec-2021.
- Mourad B and Cimini M System Description: Lang-n-Change - A Tool for Transforming Languages Functional and Logic Programming, (198-214)
- Mourad B and Cimini M A Calculus for Language Transformations SOFSEM 2020: Theory and Practice of Computer Science, (547-555)
- de Boer F, Johnsen E, Pun K and Tapia Tarifa S From SOS to Asynchronously Communicating Actors Software Engineering and Formal Methods, (269-275)
- Bartha S and Cheney J Towards Meta-interpretive Learning of Programming Language Semantics Inductive Logic Programming, (16-25)
- Cimini M Early Experience in Teaching the Basics of Functional Language Design with a Language Type Checker Trends in Functional Programming, (21-37)
- Fuentes Carranza J and Fong P Brokering Policies and Execution Monitors for IoT Middleware Proceedings of the 24th ACM Symposium on Access Control Models and Technologies, (49-60)
- Florence S, You S, Tov J and Findler R (2019). A calculus for Esterel: if can, can. if no can, no can., Proceedings of the ACM on Programming Languages, 3:POPL, (1-29), Online publication date: 2-Jan-2019.
- Pombrio J and Krishnamurthi S (2018). Inferring type rules for syntactic sugar, ACM SIGPLAN Notices, 53:4, (812-825), Online publication date: 2-Dec-2018.
- Sainati D and Sampson A LambdaLab: an interactive λ-calculus reducer for learning Proceedings of the 2018 ACM SIGPLAN Workshop on SPLASH-E, (10-19)
- Swalens J, De Koster J and De Meuter W Chocola: integrating futures, actors, and transactions Proceedings of the 8th ACM SIGPLAN International Workshop on Programming Based on Actors, Agents, and Decentralized Control, (33-43)
- van Antwerpen H, Bach Poulsen C, Rouvoet A and Visser E (2018). Scopes as types, Proceedings of the ACM on Programming Languages, 2:OOPSLA, (1-30), Online publication date: 24-Oct-2018.
- Delfino T and Ribeiro R Towards certified virtual machine-based regular expression parsing Proceedings of the XXII Brazilian Symposium on Programming Languages, (67-74)
- Vergu V and Visser E Specializing a meta-interpreter Proceedings of the 15th International Conference on Managed Languages & Runtimes, (1-14)
- Stampoulis A and Chlipala A (2018). Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam, Proceedings of the ACM on Programming Languages, 2:ICFP, (1-30), Online publication date: 30-Jul-2018.
- Wand M, Culpepper R, Giannakopoulos T and Cobb A (2018). Contextual equivalence for a probabilistic language with continuous random variables and recursion, Proceedings of the ACM on Programming Languages, 2:ICFP, (1-30), Online publication date: 30-Jul-2018.
- Pombrio J and Krishnamurthi S Inferring type rules for syntactic sugar Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, (812-825)
- Ge R and Garcia R (2017). Refining semantics for multi-stage programming, ACM SIGPLAN Notices, 52:12, (2-14), Online publication date: 1-Dec-2017.
- Soldevila M, Ziliani B, Silvestre B, Fridlender D and Mascarenhas F (2017). Decoding Lua: formal semantics for the developer and the semanticist, ACM SIGPLAN Notices, 52:11, (75-86), Online publication date: 1-Dec-2017.
- Soldevila M, Ziliani B, Silvestre B, Fridlender D and Mascarenhas F Decoding Lua: formal semantics for the developer and the semanticist Proceedings of the 13th ACM SIGPLAN International Symposium on on Dynamic Languages, (75-86)
- Ge R and Garcia R Refining semantics for multi-stage programming Proceedings of the 16th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, (2-14)
- Madsen M, Lhoták O and Tip F (2017). A model for reasoning about JavaScript promises, Proceedings of the ACM on Programming Languages, 1:OOPSLA, (1-24), Online publication date: 12-Oct-2017.
- Biernacka M, Biernacki D, Lenglet S, Polesiuk P, Pous D and Schmitt A Fully abstract encodings of λ-calculus in hocore through abstract machines Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, (1-12)
- Omar C and Aldrich J (2016). Programmable semantic fragments: the design and implementation of typy, ACM SIGPLAN Notices, 52:3, (81-92), Online publication date: 12-May-2017.
- Gibbons J APLicative Programming with Naperian Functors Programming Languages and Systems, (556-583)
- Stefănescu A, Park D, Yuwen S, Li Y and Roşu G (2016). Semantics-based program verifiers for all languages, ACM SIGPLAN Notices, 51:10, (74-91), Online publication date: 5-Dec-2016.
- Dimoulas C, New M, Findler R and Felleisen M (2016). Oh Lord, please don't let contracts be misunderstood (functional pearl), ACM SIGPLAN Notices, 51:9, (117-131), Online publication date: 5-Dec-2016.
- Seidel E, Jhala R and Weimer W (2016). Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong), ACM SIGPLAN Notices, 51:9, (228-242), Online publication date: 5-Dec-2016.
- Omar C and Aldrich J Programmable semantic fragments: the design and implementation of typy Proceedings of the 2016 ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, (81-92)
- Stefănescu A, Park D, Yuwen S, Li Y and Roşu G Semantics-based program verifiers for all languages Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, (74-91)
- Dimoulas C, New M, Findler R and Felleisen M Oh Lord, please don't let contracts be misunderstood (functional pearl) Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, (117-131)
- Seidel E, Jhala R and Weimer W Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong) Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, (228-242)
- Kent A, Kempe D and Tobin-Hochstadt S (2016). Occurrence typing modulo theories, ACM SIGPLAN Notices, 51:6, (296-309), Online publication date: 1-Aug-2016.
- Kent A, Kempe D and Tobin-Hochstadt S Occurrence typing modulo theories Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, (296-309)
- Capriccioli A, Servetto M and Zucca E (2016). An Imperative Pure Calculus, Electronic Notes in Theoretical Computer Science (ENTCS), 322:C, (87-102), Online publication date: 18-Apr-2016.
- Lorenzen F and Erdweg S (2016). Sound type-dependent syntactic language extension, ACM SIGPLAN Notices, 51:1, (204-216), Online publication date: 8-Apr-2016.
- Bračevac O, Erdweg S, Salvaneschi G and Mezini M CPL: a core language for cloud computing Proceedings of the 15th International Conference on Modularity, (94-105)
- Lorenzen F and Erdweg S Sound type-dependent syntactic language extension Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (204-216)
- Madsen M, Tip F and Lhoták O (2015). Static analysis of event-driven Node.js JavaScript applications, ACM SIGPLAN Notices, 50:10, (505-519), Online publication date: 18-Dec-2015.
- Madsen M, Tip F and Lhoták O Static analysis of event-driven Node.js JavaScript applications Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, (505-519)
- Tan Y, Owens S and Kumar R A verified type system for CakeML Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages, (1-12)
- Svensson B, Vollmer M, Holk E, McDonell T and Newton R Converting data-parallelism to task-parallelism by rewrites: purely functional programs across multiple GPUs Proceedings of the 4th ACM SIGPLAN Workshop on Functional High-Performance Computing, (12-22)
- Glaze D and Van Horn D (2014). Abstracting abstract control, ACM SIGPLAN Notices, 50:2, (11-22), Online publication date: 12-May-2015.
- Visser E, Wachsmuth G, Tolmach A, Neron P, Vergu V, Passalaqua A and Konat G A Language Designer's Workbench Proceedings of the 2014 ACM International Symposium on New Ideas, New Paradigms, and Reflections on Programming & Software, (95-111)
- Glaze D and Van Horn D Abstracting abstract control Proceedings of the 10th ACM Symposium on Dynamic languages, (11-22)
- Nunes-Harwitt A From Naïve to Norvig On Deriving a PROLOG Compiler Proceedings of ILC 2014 on 8th International Lisp Conference, (70-78)
- Pombrio J and Krishnamurthi S Resugaring Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, (361-371)
- Pombrio J and Krishnamurthi S (2014). Resugaring, ACM SIGPLAN Notices, 49:6, (361-371), Online publication date: 5-Jun-2014.
- Visser E Separation of concerns in language definition Proceedings of the companion publication of the 13th international conference on Modularity, (1-2)
- Slepak J, Shivers O and Manolios P An Array-Oriented Language with Static Rank Polymorphism Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410, (27-46)
- Garnock-Jones T, Tobin-Hochstadt S and Felleisen M The Network as a Language Construct Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410, (473-492)
- Flatt M (2013). Submodules in racket, ACM SIGPLAN Notices, 49:3, (13-22), Online publication date: 5-Mar-2014.
- Tanter É, Figueroa I and Tabareau N (2014). Execution levels for aspect-oriented programming, Science of Computer Programming, 80:PB, (311-342), Online publication date: 1-Feb-2014.
- Chang S and Felleisen M (2014). Profiling for laziness, ACM SIGPLAN Notices, 49:1, (349-360), Online publication date: 13-Jan-2014.
- Kuper L, Turon A, Krishnaswami N and Newton R (2014). Freeze after writing, ACM SIGPLAN Notices, 49:1, (257-270), Online publication date: 13-Jan-2014.
- Kumar R, Myreen M, Norrish M and Owens S (2014). CakeML, ACM SIGPLAN Notices, 49:1, (179-191), Online publication date: 13-Jan-2014.
- Chang S and Felleisen M Profiling for laziness Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (349-360)
- Kuper L, Turon A, Krishnaswami N and Newton R Freeze after writing Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (257-270)
- Kumar R, Myreen M, Norrish M and Owens S CakeML Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (179-191)
- Zerny I (2013). On graph rewriting, reduction, and evaluation in the presence of cycles, Higher-Order and Symbolic Computation, 26:1-4, (63-84), Online publication date: 1-Dec-2013.
- St-Amour V and Toronto N (2013). Experience report, ACM SIGPLAN Notices, 48:9, (351-356), Online publication date: 12-Nov-2013.
- Glaze D, Labich N, Might M and Van Horn D (2013). Optimizing abstract abstract machines, ACM SIGPLAN Notices, 48:9, (443-454), Online publication date: 12-Nov-2013.
- Lorenzen F and Erdweg S (2013). Modular and automated type-soundness verification for language extensions, ACM SIGPLAN Notices, 48:9, (331-342), Online publication date: 12-Nov-2013.
- Dimoulas C, Findler R and Felleisen M (2013). Option contracts, ACM SIGPLAN Notices, 48:10, (475-494), Online publication date: 12-Nov-2013.
- Politz J, Martinez A, Milano M, Warren S, Patterson D, Li J, Chitipothu A and Krishnamurthi S (2013). Python, ACM SIGPLAN Notices, 48:10, (217-232), Online publication date: 12-Nov-2013.
- Strickland T, Dimoulas C, Takikawa A and Felleisen M (2013). Contracts for First-Class Classes, ACM Transactions on Programming Languages and Systems, 35:3, (1-58), Online publication date: 1-Nov-2013.
- Torlak E and Bodik R Growing solver-aided languages with rosette Proceedings of the 2013 ACM international symposium on New ideas, new paradigms, and reflections on programming & software, (135-152)
- Dimoulas C, Findler R and Felleisen M Option contracts Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications, (475-494)
- Politz J, Martinez A, Milano M, Warren S, Patterson D, Li J, Chitipothu A and Krishnamurthi S Python Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications, (217-232)
- Flatt M Submodules in racket Proceedings of the 12th international conference on Generative programming: concepts & experiences, (13-22)
- St-Amour V and Toronto N Experience report Proceedings of the 18th ACM SIGPLAN international conference on Functional programming, (351-356)
- Glaze D, Labich N, Might M and Van Horn D Optimizing abstract abstract machines Proceedings of the 18th ACM SIGPLAN international conference on Functional programming, (443-454)
- Lorenzen F and Erdweg S Modular and automated type-soundness verification for language extensions Proceedings of the 18th ACM SIGPLAN international conference on Functional programming, (331-342)
- Kuper L and Newton R LVars Proceedings of the 2nd ACM SIGPLAN workshop on Functional high-performance computing, (71-84)
- Simmons R and Zerny I A logical correspondence between natural semantics and abstract machines Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, (109-119)
- Danvy O and Zerny I A synthetic operational account of call-by-need evaluation Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, (97-108)
- Midtgaard J, Ramsey N and Larsen B Engineering definitional interpreters Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, (121-132)
- Servetto M and Groves L True small-step reduction for imperative object oriented languages Proceedings of the 15th Workshop on Formal Techniques for Java-like Programs, (1-7)
- Gilray T and Might M A Survey of Polyvariance in Abstract Interpretations Revised Selected Papers of the 14th International Symposium on Trends in Functional Programming - Volume 8322, (134-148)
- Toledo R and Tanter É Secure and modular access control with aspects Proceedings of the 12th annual international conference on Aspect-oriented software development, (157-170)
- Bettini L Implementing Java-like languages in Xtext with Xsemantics Proceedings of the 28th Annual ACM Symposium on Applied Computing, (1559-1564)
- Politz J, Carroll M, Lerner B, Pombrio J and Krishnamurthi S (2012). A tested semantics for getters, setters, and eval in JavaScript, ACM SIGPLAN Notices, 48:2, (1-16), Online publication date: 23-Jan-2013.
- Klein C, Flatt M and Findler R (2012). The Racket virtual machine and randomized testing, Higher-Order and Symbolic Computation, 25:2-4, (209-253), Online publication date: 1-Dec-2012.
- Takikawa A, Strickland T, Dimoulas C, Tobin-Hochstadt S and Felleisen M (2012). Gradual typing for first-class classes, ACM SIGPLAN Notices, 47:10, (793-810), Online publication date: 15-Nov-2012.
- Rosu G and Stefanescu A (2012). Checking reachability using matching logic, ACM SIGPLAN Notices, 47:10, (555-574), Online publication date: 15-Nov-2012.
- Politz J, Carroll M, Lerner B, Pombrio J and Krishnamurthi S A tested semantics for getters, setters, and eval in JavaScript Proceedings of the 8th symposium on Dynamic languages, (1-16)
- Takikawa A, Strickland T, Dimoulas C, Tobin-Hochstadt S and Felleisen M Gradual typing for first-class classes Proceedings of the ACM international conference on Object oriented programming systems languages and applications, (793-810)
- Rosu G and Stefanescu A Checking reachability using matching logic Proceedings of the ACM international conference on Object oriented programming systems languages and applications, (555-574)
- Politz J, Quay-de la Vallee H and Krishnamurthi S Progressive types Proceedings of the ACM international symposium on New ideas, new paradigms, and reflections on programming and software, (55-66)
- Myreen M and Owens S (2012). Proof-producing synthesis of ML from higher-order logic, ACM SIGPLAN Notices, 47:9, (115-126), Online publication date: 15-Oct-2012.
- Myreen M and Owens S Proof-producing synthesis of ML from higher-order logic Proceedings of the 17th ACM SIGPLAN international conference on Functional programming, (115-126)
- Roşu G and Ştefănescu A Towards a unified theory of operational and axiomatic semantics Proceedings of the 39th international colloquium conference on Automata, Languages, and Programming - Volume Part II, (351-363)
- Chang S and Felleisen M The call-by-need lambda calculus, revisited Proceedings of the 21st European conference on Programming Languages and Systems, (128-147)
- Sergey I and Clarke D Gradual ownership types Proceedings of the 21st European conference on Programming Languages and Systems, (579-599)
- Morse E, Vrvilo N, Mercer E and McCarthy J Modeling asynchronous message passing for c programs Proceedings of the 13th international conference on Verification, Model Checking, and Abstract Interpretation, (332-347)
- Klein C, McCarthy J, Jaconette S and Findler R A semantics for context-sensitive reduction semantics Proceedings of the 9th Asian conference on Programming Languages and Systems, (369-383)
- Dimoulas C and Felleisen M (2011). On contract satisfaction in a higher-order world, ACM Transactions on Programming Languages and Systems, 33:5, (1-29), Online publication date: 1-Nov-2011.
- Chang S, Barzilay E, Clements J and Felleisen M From stack traces to lazy rewriting sequences Proceedings of the 23rd international conference on Implementation and Application of Functional Languages, (100-115)
- Disney T, Flanagan C and McCarthy J Temporal higher-order contracts Proceedings of the 16th ACM SIGPLAN international conference on Functional programming, (176-188)
- Disney T, Flanagan C and McCarthy J (2011). Temporal higher-order contracts, ACM SIGPLAN Notices, 46:9, (176-188), Online publication date: 18-Sep-2011.
- Van Horn D and Might M (2011). Abstracting abstract machines, Communications of the ACM, 54:9, (101-109), Online publication date: 1-Sep-2011.
- Bettini L A DSL for writing type systems for Xtext languages Proceedings of the 9th International Conference on Principles and Practice of Programming in Java, (31-40)
- Erwig M and Walkingshaw E Semantics first! Proceedings of the 4th international conference on Software Language Engineering, (243-262)
- Figueroa I and Tanter É A semantics for execution levels with exceptions Proceedings of the 10th international workshop on Foundations of aspect-oriented languages, (7-11)
- Dimoulas C, Findler R, Flanagan C and Felleisen M Correct blame for contracts Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (215-226)
- Dimoulas C, Findler R, Flanagan C and Felleisen M (2011). Correct blame for contracts, ACM SIGPLAN Notices, 46:1, (215-226), Online publication date: 26-Jan-2011.
- Guha A and Krishnamurthi S Minding the (semantic) gap Proceedings of the FSE/SDP workshop on Future of software engineering research, (155-156)
- Klein C, Flatt M and Findler R (2010). Random testing for higher-order, stateful programs, ACM SIGPLAN Notices, 45:10, (555-566), Online publication date: 17-Oct-2010.
- Klein C, Flatt M and Findler R Random testing for higher-order, stateful programs Proceedings of the ACM international conference on Object oriented programming systems languages and applications, (555-566)
- Van Horn D and Might M (2010). Abstracting abstract machines, ACM SIGPLAN Notices, 45:9, (51-62), Online publication date: 27-Sep-2010.
- Van Horn D and Might M Abstracting abstract machines Proceedings of the 15th ACM SIGPLAN international conference on Functional programming, (51-62)
- Sakurai K and Asai K Mikibeta Proceedings of the 20th international conference on Logic-based program synthesis and transformation, (84-98)
- Guha A, Saftoiu C and Krishnamurthi S The essence of javascript Proceedings of the 24th European conference on Object-oriented programming, (126-150)
- Dingel J, Paen E, Posse E, Rahman R and Zurowska K Definition and implementation of a semantic mapping for UML-RT using a timed pi-calculus Proceedings of the Second International Workshop on Behaviour Modelling: Foundation and Applications, (1-8)
- Chang S, Van Horn D and Felleisen M Evaluating call-by-need on the control stack Proceedings of the 11th international conference on Trends in functional programming, (1-15)
- Tanter É Execution levels for aspect-oriented programming Proceedings of the 9th International Conference on Aspect-Oriented Software Development, (37-48)
- Strickland T and Felleisen M (2009). Contracts for first-class modules, ACM SIGPLAN Notices, 44:12, (27-38), Online publication date: 25-Dec-2009.
- Strickland T and Felleisen M Contracts for first-class modules Proceedings of the 5th symposium on Dynamic languages, (27-38)
Recommendations
Redex: a language for lightweight semantics engineering (keynote)
SLE 2016: Proceedings of the 2016 ACM SIGPLAN International Conference on Software Language EngineeringRedex is a programming language designed to support semantics engineers as they experiment with programming language models. To explore a model, an engineer writes down grammars, type systems, and operational semantics in a notation inspired by the ...
Kripke Semantics for Modal Substructural Logics
We introduce Kripke semantics for modal substructural logics, and prove the completeness theorems with respect to the semantics. The completeness theorems are proved using an extended Ishihara's method of canonical model construction (Ishihara, 2000). The ...