Reference. Safely Composable Type-Specific Languages
Cite
Cited by (3)
Filling typed holes with live GUIs omar-2021-filling
Reasonably programmable literal notation omar-2018-reasonably
General-purpose programming languages typically define literal notation for only a small number of common data structures, like lists. This is unsatisfying because there are many other data structures for which literal notation might be useful, e.g. finite maps, regular expressions, HTML elements, SQL queries, syntax trees for various languages and chemical structures. There may also be different implementations of each of these data structures behind a common interface that could all benefit from common literal notation. This paper introduces typed literal macros (TLMs) , which allow library providers to define new literal notation of nearly arbitrary design at any specified type or parameterized family of types. Compared to existing approaches, TLMs are uniquely reasonable . TLM clients can reason abstractly, i.e. without examining grammars or generated expansions, about types and binding. The system only needs to convey to clients, via secondary notation, the inferred segmentation of each literal body, which gives the locations and types of spliced subterms. TLM providers can reason modularly about syntactic ambiguity and expansion correctness according to clear criteria. This paper incorporates TLMs into Reason, an emerging alternative front-end for OCaml, and demonstrates, through several non-trivial case studies, how TLMs integrate with the advanced features of OCaml, including pattern matching and the module system. We also discuss optional integration with MetaOCaml, which allows TLM providers to be more confident about type correctness. Finally, we establish these abstract reasoning principles formally with a detailed type-theoretic account of expression and pattern TLMs for “core ML”.
Hazelnut: a bidirectionally typed structure editor calculus omar-2017-hazelnut
Cites 36 works (1 here)
With notes (1)
Formal verification of a realistic compiler leroy_formal_2009
This paper reports on the development and formal verification (proof of semantic preservation) of CompCert, a compiler from Clight (a large subset of the C programming language) to PowerPC assembly code, using the Coq proof assistant both for programming the compiler and for proving its correctness. Such a verified compiler is useful in the context of critical software and its formal verification: the verification of the compiler guarantees that the safety properties proved on the source code hold for the executable compiled code as well.
External (35)
- Composable user-defined operators that can express user-defined literals (2014)
- On domain-specific languages usage (why DLSs really matter) (2014)
- Safely Composable Type-Specific Languages (Technical Report CMU-ISR-14-106) (2014)
- Principled parsing for indentation-sensitive languages: revisiting landin's offside rule (2013)
- A framework for extensible languages (2013)
- Termination Analysis for Higher-Order Attribute Grammars (2013)
- Instant pickles: generating object-oriented pickler combinators for fast and extensible serialization (2013)
- Wyvern: a simple, typed, and pure object-oriented language (2013)
- Type-directed, whitespace-delimited parsing for embedded DSLs (2013)
- Parsing composed grammars with language boxes (2013)
- OWASP Top 10 2013 (2013)
- Practical Foundations for Programming Languages (2012)
- Marco: Safe, Expressive Macros for Any Language (2012)
- Managed data: modular strategies for data abstraction (2012)
- Active code completion (2012)
- SugarJ: library-based language extensibility (2011)
- Backstage Java: making a difference in metaprogramming (2011)
- The spoofax language workbench: rules for declarative specification of languages and IDEs (2010)
- The Qualitas Corpus: A Curated Collection of Java Code for Empirical Studies (2010)
- Verifiable composition of deterministic grammars (2009)
- Beyond Annotations: A Proposal for Extensible Java (XJ) (2008)
- Domain specific language implementation via compile-time meta-programming (2008)
- Context-aware scanning for parsing extensible languages (2007)
- Generalized Type-Based Disambiguation of Meta Programs with Concrete Object Syntax (2005)
- SRFI-49: Indentation-sensitive syntax (2005)
- Camlp4 - Reference Manual (2003)
- Template meta-programming for Haskell (2002)
- A Type-Theoretic Interpretation of Standard ML (2000)
- Local type inference (2000)
- OpenJava: A Class-Based Macro System for Java (2000)
- Usability Analysis of Visual Programming Environments: A 'Cognitive Dimensions' Framework (1996)
- Pregmatic: A Generator for Incremental Programming Environments (1992)
- Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory (1977)
- JetBrains MPS – Meta Programming System
- Expression Trees (C# and Visual Basic)