2 Search Results for "Kravchuk-Kirilyuk, Anastasiya"


Document
Pearl/Brave New Idea
The Dolorem Pattern: Growing a Language Through Compile-Time Function Execution (Pearl/Brave New Idea)

Authors: Simon Henniger and Nada Amin

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)


Abstract
Programming languages are often designed as static, monolithic units. As a result, they are inflexible. We show a new mechanism of programming language design that allows to more flexible languages: by using compile-time function execution and metaprogramming, we implement a language mostly in itself. Our approach is usable for creating feature-rich, yet low-overhead system programming languages. We illustrate it on two systems, one that lowers to C and one that lowers to LLVM.

Cite as

Simon Henniger and Nada Amin. The Dolorem Pattern: Growing a Language Through Compile-Time Function Execution (Pearl/Brave New Idea). In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 41:1-41:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{henniger_et_al:LIPIcs.ECOOP.2023.41,
  author =	{Henniger, Simon and Amin, Nada},
  title =	{{The Dolorem Pattern: Growing a Language Through Compile-Time Function Execution}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{41:1--41:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.41},
  URN =		{urn:nbn:de:0030-drops-182343},
  doi =		{10.4230/LIPIcs.ECOOP.2023.41},
  annote =	{Keywords: extensible languages, meta programming, macros, program generation, compilation}
}
Document
Eta-Equivalence in Core Dependent Haskell

Authors: Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, and Stephanie Weirich

Published in: LIPIcs, Volume 175, 25th International Conference on Types for Proofs and Programs (TYPES 2019)


Abstract
We extend the core semantics for Dependent Haskell with rules for η-equivalence. This semantics is defined by two related calculi, Systems D and DC. The first is a Curry-style dependently-typed language with nontermination, irrelevant arguments, and equality abstraction. The second, inspired by the Glasgow Haskell Compiler’s core language FC, is the explicitly-typed analogue of System D, suitable for implementation in GHC. Our work builds on and extends the existing metatheory for these systems developed using the Coq proof assistant.

Cite as

Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, and Stephanie Weirich. Eta-Equivalence in Core Dependent Haskell. In 25th International Conference on Types for Proofs and Programs (TYPES 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 175, pp. 7:1-7:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


Copy BibTex To Clipboard

@InProceedings{kravchukkirilyuk_et_al:LIPIcs.TYPES.2019.7,
  author =	{Kravchuk-Kirilyuk, Anastasiya and Voizard, Antoine and Weirich, Stephanie},
  title =	{{Eta-Equivalence in Core Dependent Haskell}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{7:1--7:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Bezem, Marc and Mahboubi, Assia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2019.7},
  URN =		{urn:nbn:de:0030-drops-130716},
  doi =		{10.4230/LIPIcs.TYPES.2019.7},
  annote =	{Keywords: Dependent types, Haskell, Irrelevance, Eta-equivalence}
}
  • Refine by Author
  • 1 Amin, Nada
  • 1 Henniger, Simon
  • 1 Kravchuk-Kirilyuk, Anastasiya
  • 1 Voizard, Antoine
  • 1 Weirich, Stephanie

  • Refine by Classification
  • 1 Software and its engineering → Compilers
  • 1 Software and its engineering → Functional languages
  • 1 Software and its engineering → Language features
  • 1 Software and its engineering → Polymorphism
  • 1 Theory of computation → Type theory

  • Refine by Keyword
  • 1 Dependent types
  • 1 Eta-equivalence
  • 1 Haskell
  • 1 Irrelevance
  • 1 compilation
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2020
  • 1 2023

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail