6 Search Results for "Rompf, Tiark"

Document
DOI: 10.4230/LIPIcs.ECOOP.2024.33
Compiling with Arrays

Authors: David Richter, Timon Böhler, Pascal Weisenburger, and Mira Mezini

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
Linear algebra computations are foundational for neural networks and machine learning, often handled through arrays. While many functional programming languages feature lists and recursion, arrays in linear algebra demand constant-time access and bulk operations. To bridge this gap, some languages represent arrays as (eager) functions instead of lists. In this paper, we connect this idea to a formal logical foundation by interpreting functions as the usual negative types from polarized type theory, and arrays as the corresponding dual positive version of the function type. Positive types are defined to have a single elimination form whose computational interpretation is pattern matching. Just like (positive) product types bind two variables during pattern matching, (positive) array types bind variables with multiplicity during pattern matching. We follow a similar approach for Booleans by introducing conditionally-defined variables. The positive formulation for the array type enables us to combine typed partial evaluation and common subexpression elimination into an elegant algorithm whose result enjoys a property we call maximal fission, which we argue can be beneficial for further optimizations. For this purpose, we present the novel intermediate representation indexed administrative normal form (A_{i}NF), which relies on the formal logical foundation of the positive formulation for the array type to facilitate maximal loop fission and subsequent optimizations. A_{i}NF is normal with regard to commuting conversion for both let-bindings and for-loops, leading to flat and maximally fissioned terms. We mechanize the translation and normalization from a simple surface language to A_{i}NF, establishing that the process terminates, preserves types, and produces maximally fissioned terms.
Cite as

David Richter, Timon Böhler, Pascal Weisenburger, and Mira Mezini. Compiling with Arrays. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 33:1-33:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{richter_et_al:LIPIcs.ECOOP.2024.33,
  author =	{Richter, David and B\"{o}hler, Timon and Weisenburger, Pascal and Mezini, Mira},
  title =	{{Compiling with Arrays}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{33:1--33:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.33},
  URN =		{urn:nbn:de:0030-drops-208823},
  doi =		{10.4230/LIPIcs.ECOOP.2024.33},
  annote =	{Keywords: array languages, functional programming, domain-specific languages, normalization by evaluation, common subexpression elimination, polarity, positive function type, intrinsic types}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.15
What If We Don't Pop the Stack? The Return of 2nd-Class Values

Authors: Anxhelo Xhebraj, Oliver Bračevac, Guannan Wei, and Tiark Rompf

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Using a stack for managing the local state of procedures as popularized by Algol is a simple but effective way to achieve a primitive form of automatic memory management. Hence, the call stack remains the backbone of most programming language runtimes to the present day. However, the appealing simplicity of the call stack model comes at the price of strictly enforced limitations: since every function return pops the stack, it is difficult to return stack-allocated data from a callee upwards to its caller - especially variable-size data such as closures. This paper proposes a solution by introducing a small tweak to the usual stack semantics. We design a type system that tracks the underlying storage mode of values, and when a function returns a stack-allocated value, we just don't pop the stack! Instead, the stack frame is de-allocated together with a parent the next time a heap-allocated value or primitive is returned. We identify a range of use cases where this delayed-popping strategy is beneficial, ranging from closures to trait objects to other types of variable-size data. Our evaluation shows that this execution model reduces heap and GC pressure and recovers spatial locality of programs improving execution time between 10% and 25% with respect to standard execution.
Cite as

Anxhelo Xhebraj, Oliver Bračevac, Guannan Wei, and Tiark Rompf. What If We Don't Pop the Stack? The Return of 2nd-Class Values. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 15:1-15:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{xhebraj_et_al:LIPIcs.ECOOP.2022.15,
  author =	{Xhebraj, Anxhelo and Bra\v{c}evac, Oliver and Wei, Guannan and Rompf, Tiark},
  title =	{{What If We Don't Pop the Stack? The Return of 2nd-Class Values}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{15:1--15:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.15},
  URN =		{urn:nbn:de:0030-drops-162430},
  doi =		{10.4230/LIPIcs.ECOOP.2022.15},
  annote =	{Keywords: Call stack, closures, stack allocation, memory management, 2nd-class values, capabilities, effects}
}
Document
Artifact
DOI: 10.4230/DARTS.8.2.26
What If We Don't Pop the Stack? The Return of 2nd-Class Values (Artifact)

Authors: Anxhelo Xhebraj, Oliver Bračevac, Guannan Wei, and Tiark Rompf

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
The main paper presents λ^{1/2}_{↩}, a type system and operational semantics with 2nd-class values and delayed stack reclamation. This artifact contains a compiler implementation of the calculus in Scala Native, the code for the case studies shown in the paper, and code for reproducing the evaluation.
Cite as

Anxhelo Xhebraj, Oliver Bračevac, Guannan Wei, and Tiark Rompf. What If We Don't Pop the Stack? The Return of 2nd-Class Values (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 26:1-26:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{xhebraj_et_al:DARTS.8.2.26,
  author =	{Xhebraj, Anxhelo and Bra\v{c}evac, Oliver and Wei, Guannan and Rompf, Tiark},
  title =	{{What If We Don't Pop the Stack? The Return of 2nd-Class Values (Artifact)}},
  pages =	{26:1--26:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Xhebraj, Anxhelo and Bra\v{c}evac, Oliver and Wei, Guannan and Rompf, Tiark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.26},
  URN =		{urn:nbn:de:0030-drops-162247},
  doi =		{10.4230/DARTS.8.2.26},
  annote =	{Keywords: Call stack, closures, stack allocation, memory management, 2nd-class values, capabilities, effects}
}
Document
DOI: 10.4230/DARTS.3.2.5
Towards Strong Normalization for Dependent Object Types (DOT) (Artifact)

Authors: Fei Wang and Tiark Rompf

Published in: DARTS, Volume 3, Issue 2, Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
This artifact provides the fully mechanized proof of strong normalization for D_{<:} , a variant of (Dependent Object Types) DOT (Rompf & Amin, 2016) that excludes recursive functions and recursive types. The intersection type and recursive self type are further integrated, moving towards DOT. The key proof idea follows the method of Girard (Girard, 1972) and Tait (Tait, 1967).
Cite as

Fei Wang and Tiark Rompf. Towards Strong Normalization for Dependent Object Types (DOT) (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 5:1-5:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{wang_et_al:DARTS.3.2.5,
  author =	{Wang, Fei and Rompf, Tiark},
  title =	{{Towards Strong Normalization for Dependent Object Types (DOT) (Artifact)}},
  pages =	{5:1--5:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2017},
  volume =	{3},
  number =	{2},
  editor =	{Wang, Fei and Rompf, Tiark},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.5},
  URN =		{urn:nbn:de:0030-drops-72869},
  doi =		{10.4230/DARTS.3.2.5},
  annote =	{Keywords: Scala, DOT, strong normalization, logical relations, recursive types}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2017.27
Towards Strong Normalization for Dependent Object Types (DOT)

Authors: Fei Wang and Tiark Rompf

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
The Dependent Object Types (DOT) family of calculi has been proposed as a new theoretic foundation for Scala and similar languages, unifying functional programming, object oriented programming and ML-style module systems. Following the recent type soundness proof for DOT, the present paper aims to establish stronger meta-theoretic properties. The main result is a fully mechanized proof of strong normalization for D_<:, a variant of DOT that excludes recursive functions and recursive types. We further discuss techniques and challenges for adding recursive types while maintaining strong normalization, and demonstrate that certain variants of recursive self types can be integrated successfully.
Cite as

Fei Wang and Tiark Rompf. Towards Strong Normalization for Dependent Object Types (DOT). In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 27:1-27:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{wang_et_al:LIPIcs.ECOOP.2017.27,
  author =	{Wang, Fei and Rompf, Tiark},
  title =	{{Towards Strong Normalization for Dependent Object Types (DOT)}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{27:1--27:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.27},
  URN =		{urn:nbn:de:0030-drops-72763},
  doi =		{10.4230/LIPIcs.ECOOP.2017.27},
  annote =	{Keywords: Scala, DOT, strong normalization, logical relations, recursive types}
}
Document
DOI: 10.4230/LIPIcs.SNAPL.2015.238
Go Meta! A Case for Generative Programming and DSLs in Performance Critical Systems

Authors: Tiark Rompf, Kevin J. Brown, HyoukJoong Lee, Arvind K. Sujeeth, Manohar Jonnalagedda, Nada Amin, Georg Ofenbeck, Alen Stojanov, Yannis Klonatos, Mohammad Dashti, Christoph Koch, Markus Püschel, and Kunle Olukotun

Published in: LIPIcs, Volume 32, 1st Summit on Advances in Programming Languages (SNAPL 2015)

Abstract
Most performance critical software is developed using very low-level techniques. We argue that this needs to change, and that generative programming is an effective avenue to enable the use of high-level languages and programming techniques in many such circumstances.
Cite as

Tiark Rompf, Kevin J. Brown, HyoukJoong Lee, Arvind K. Sujeeth, Manohar Jonnalagedda, Nada Amin, Georg Ofenbeck, Alen Stojanov, Yannis Klonatos, Mohammad Dashti, Christoph Koch, Markus Püschel, and Kunle Olukotun. Go Meta! A Case for Generative Programming and DSLs in Performance Critical Systems. In 1st Summit on Advances in Programming Languages (SNAPL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 32, pp. 238-261, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{rompf_et_al:LIPIcs.SNAPL.2015.238,
  author =	{Rompf, Tiark and Brown, Kevin J. and Lee, HyoukJoong and Sujeeth, Arvind K. and Jonnalagedda, Manohar and Amin, Nada and Ofenbeck, Georg and Stojanov, Alen and Klonatos, Yannis and Dashti, Mohammad and Koch, Christoph and P\"{u}schel, Markus and Olukotun, Kunle},
  title =	{{Go Meta! A Case for Generative Programming and DSLs in Performance Critical Systems}},
  booktitle =	{1st Summit on Advances in Programming Languages (SNAPL 2015)},
  pages =	{238--261},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-80-4},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{32},
  editor =	{Ball, Thomas and Bodík, Rastislav and Krishnamurthi, Shriram and Lerner, Benjamin S. and Morriset, Greg},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SNAPL.2015.238},
  URN =		{urn:nbn:de:0030-drops-50295},
  doi =		{10.4230/LIPIcs.SNAPL.2015.238},
  annote =	{Keywords: Performance, Generative Programming, Staging, DSLs}
}
  • Refine by Author
  • 5 Rompf, Tiark
  • 2 Bračevac, Oliver
  • 2 Wang, Fei
  • 2 Wei, Guannan
  • 2 Xhebraj, Anxhelo
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 2 2nd-class values
  • 2 Call stack
  • 2 DOT
  • 2 Scala
  • 2 capabilities
  • Show More...

  • Refine by Type
  • 6 document

  • Refine by Publication Year
  • 2 2017
  • 2 2022
  • 1 2015
  • 1 2024

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
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact