main.bib

@inproceedings {TALx86,
  author = {Greg Morrisett et al},
  title = {TALx86: A Realistic Typed Assembly Language},
  year = {1999},
  booktitle = {Proceedings of the ACM SIGPLAN 1999 Workshop on Languages, Compilers, and Tools for Embedded Systems},
  pages = {25--35},
  url = {https://www.cs.cornell.edu/talc/papers/talx86-wcsss.pdf}
}

@inproceedings{DTAL,
  author = {Xi, Hongwei and Harper, Robert},
  title = {A Dependently Typed Assembly Language},
  year = {2001},
  isbn = {1581134150},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  url = {https://doi.org/10.1145/507635.507657},
  doi = {10.1145/507635.507657},
  abstract = {We present a dependently typed assembly language (DTAL) in which the type system supports the use of a restricted form of dependent types, reaping some benefits of dependent types at the assembly level. DTAL improves upon TAL , enabling certain important compiler optimizations such as run-time array bound check elimination and tag check elimination. Also, DTAL formally addresses the issue of representing sum types at assembly level, making it suitable for handling not only datatypes in ML but also dependent datatypes in Dependent ML (DML).},
  booktitle = {Proceedings of the Sixth ACM SIGPLAN International Conference on Functional Programming},
  pages = {169–180},
  numpages = {12},
  location = {Florence, Italy},
  series = {ICFP '01}
}

@article{FunTAL,
  author    = {Daniel Patterson and
               Jamie Perconti and
               Christos Dimoulas and
               Amal Ahmed},
  title     = {FunTAL: Reasonably Mixing a Functional Language with Assembly},
  journal   = {CoRR},
  volume    = {abs/1711.03871},
  year      = {2017},
  url       = {http://arxiv.org/abs/1711.03871},
  archivePrefix = {arXiv},
  eprint    = {1711.03871},
  timestamp = {Mon, 13 Aug 2018 16:46:43 +0200},
  biburl    = {https://dblp.org/rec/journals/corr/abs-1711-03871.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{STAL,
  author    = {Morrisett, Greg
               and Crary, Karl
               and Glew, Neal
               and Walker, David},
  editor    = {Leroy, Xavier
               and Ohori, Atsushi},
  title     = {Stack-based Typed Assembly Language},
  booktitle = {Types in Compilation},
  year      = {1998},
  publisher = {Springer Berlin Heidelberg},
  address   = {Berlin, Heidelberg},
  pages     = {28--52},
  abstract  = {In previous work, we presented a Typed Assembly Language (TAL). TAL is sufficiently expressive to serve as a target language for compilers of high-level languages such as ML. This work assumed such a compiler would perform a continuation-passing style transform and eliminate the control stack by heap-allocating activation records. However, most compilers are based on stack allocation. This paper presents STAL, an extension of TAL with stack constructs and stack types to support the stack allocation style. We show that STAL is sufficiently expressive to support languages such as Java, Pascal, and ML; constructs such as exceptions and displays; and optimizations such as tail call elimination and callee-saves registers. This paper also formalizes the typing connection between CPS-based compilation and stack-based compilation and illustrates how STAL can formally model calling conventions by specifying them as formal translations of source function types to STAL types.},
  isbn      = {978-3-540-68308-7}
}

@inproceedings{mixfix-operators,
  author = {Danielsson, Nils Anders and Norell, Ulf},
  title = {Parsing Mixfix Operators},
  year = {2008},
  isbn = {9783642244513},
  publisher = {Springer-Verlag},
  address = {Berlin, Heidelberg},
  abstract = {A simple grammar scheme for expressions containing mixfix operators is presented. The scheme is parameterised by a precedence relation which is only restricted to be a directed acyclic graph; this makes it possible to build up precedence relations in a modular way. Efficient and simple implementations of parsers for languages with user-defined mixfix operators, based on the grammar scheme, are also discussed. In the future we plan to replace the support for mixfix operators in the language Agda with a grammar scheme and an implementation based on this work.},
  booktitle = {Proceedings of the 20th International Conference on Implementation and Application of Functional Languages},
  pages = {80–99},
  numpages = {20},
  location = {Hatfield, UK},
  series = {IFL'08}
}