Reference. Safely Composable Type-Specific Languages

Cite

Cite as @omar-2014-safely (helia, typst) · \cite{omar-2014-safely} (LaTeX)
BibTeX
bibtex · 1 line
@inbook{omar-2014-safely, title={Safely Composable Type-Specific Languages}, ISBN={9783662442029}, ISSN={1611-3349}, url={http://dx.doi.org/10.1007/978-3-662-44202-9_5}, DOI={10.1007/978-3-662-44202-9_5}, booktitle={ECOOP 2014 – Object-Oriented Programming}, publisher={Springer Berlin Heidelberg}, author={Omar, Cyrus and Kurilova, Darya and Nistor, Ligia and Chung, Benjamin and Potanin, Alex and Aldrich, Jonathan}, year={2014}, pages={105–130} }
hayagriva YAML (typst)
yaml · 21 lines
omar-2014-safely:
  type: chapter
  title: Safely Composable Type-Specific Languages
  author:
  - Omar, Cyrus
  - Kurilova, Darya
  - Nistor, Ligia
  - Chung, Benjamin
  - Potanin, Alex
  - Aldrich, Jonathan
  date: 2014
  page-range: 105-130
  url: http://dx.doi.org/10.1007/978-3-662-44202-9_5
  serial-number:
    doi: 10.1007/978-3-662-44202-9_5
    isbn: '9783662442029'
    issn: 1611-3349
  parent:
    type: book
    title: ECOOP 2014 – Object-Oriented Programming
    publisher: Springer Berlin Heidelberg
Cited by (3)

Filling typed holes with live GUIs omar-2021-filling

PDF · DOI · pldb

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”.
PDF · DOI · pldb

Hazelnut: a bidirectionally typed structure editor calculus omar-2017-hazelnut

PDF · DOI · arXiv · pldb
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.
DOI
External (35)
omar-2014-safely reference entries/refs/omar-2014-safely/omar-2014-safely.hel