4 Search Results for "Downen, Paul"

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.FSCD.2024.23
Mirroring Call-By-Need, or Values Acting Silly

Authors: Beniamino Accattoli and Adrienne Lancelot

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Call-by-need evaluation for the λ-calculus can be seen as merging the best of call-by-name and call-by-value, namely the wise erasing behaviour of the former and the wise duplicating behaviour of the latter. To better understand how duplication and erasure can be combined, we design a degenerated calculus, dubbed call-by-silly, that is symmetric to call-by-need in that it merges the worst of call-by-name and call-by-value, namely silly duplications by-name and silly erasures by-value. We validate the design of the call-by-silly calculus via rewriting properties and multi types. In particular, we mirror the main theorem about call-by-need - that is, its operational equivalence with call-by-name - showing that call-by-silly and call-by-value induce the same contextual equivalence. This fact shows the blindness with respect to efficiency of call-by-value contextual equivalence. We also define a call-by-silly strategy and measure its length via tight multi types. Lastly, we prove that the call-by-silly strategy computes evaluation sequences of maximal length in the calculus.
Cite as

Beniamino Accattoli and Adrienne Lancelot. Mirroring Call-By-Need, or Values Acting Silly. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 23:1-23:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.FSCD.2024.23,
  author =	{Accattoli, Beniamino and Lancelot, Adrienne},
  title =	{{Mirroring Call-By-Need, or Values Acting Silly}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{23:1--23:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.23},
  URN =		{urn:nbn:de:0030-drops-203527},
  doi =		{10.4230/LIPIcs.FSCD.2024.23},
  annote =	{Keywords: Lambda calculus, intersection types, call-by-value, call-by-need}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2021.1
Duality in Action (Invited Talk)

Authors: Paul Downen and Zena M. Ariola

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
The duality between "true" and "false" is a hallmark feature of logic. We show how this duality can be put to use in the theory and practice of programming languages and their implementations, too. Starting from a foundation of constructive logic as dialogues, we illustrate how it describes a symmetric language for computation, and survey several applications of the dualities found therein.
Cite as

Paul Downen and Zena M. Ariola. Duality in Action (Invited Talk). In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 1:1-1:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{downen_et_al:LIPIcs.FSCD.2021.1,
  author =	{Downen, Paul and Ariola, Zena M.},
  title =	{{Duality in Action}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{1:1--1:32},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.1},
  URN =		{urn:nbn:de:0030-drops-142390},
  doi =		{10.4230/LIPIcs.FSCD.2021.1},
  annote =	{Keywords: Duality, Logic, Curry-Howard, Sequent Calculus, Rewriting, Compilation}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.21
Beyond Polarity: Towards a Multi-Discipline Intermediate Language with Sharing

Authors: Paul Downen and Zena M. Ariola

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
The study of polarity in computation has revealed that an "ideal" programming language combines both call-by-value and call-by-name evaluation; the two calling conventions are each ideal for half the types in a programming language. But this binary choice leaves out call-by-need which is used in practice to implement lazy-by-default languages like Haskell. We show how the notion of polarity can be extended beyond the value/name dichotomy to include call-by-need by only adding a mechanism for sharing and the extra polarity shifts to connect them, which is enough to compile a Haskell-like functional language with user-defined types.
Cite as

Paul Downen and Zena M. Ariola. Beyond Polarity: Towards a Multi-Discipline Intermediate Language with Sharing. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{downen_et_al:LIPIcs.CSL.2018.21,
  author =	{Downen, Paul and Ariola, Zena M.},
  title =	{{Beyond Polarity: Towards a Multi-Discipline Intermediate Language with Sharing}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{21:1--21:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.21},
  URN =		{urn:nbn:de:0030-drops-96886},
  doi =		{10.4230/LIPIcs.CSL.2018.21},
  annote =	{Keywords: call-by-need, polarity, call-by-push-value, control}
}
  • Refine by Author
  • 2 Ariola, Zena M.
  • 2 Downen, Paul
  • 1 Accattoli, Beniamino
  • 1 Böhler, Timon
  • 1 Lancelot, Adrienne
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Domain specific languages
  • 1 Theory of computation → Lambda calculus
  • 1 Theory of computation → Logic
  • 1 Theory of computation → Type structures

  • Refine by Keyword
  • 2 call-by-need
  • 2 polarity
  • 1 Compilation
  • 1 Curry-Howard
  • 1 Duality
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2024
  • 1 2018
  • 1 2021

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 Imprint Privacy Contact