5 Search Results for "Amin, Nada"

Document
DOI: 10.4230/LIPIcs.CSL.2026.37
Towards the Type Safety of Pure Subtype Systems

Authors: Valentin Pasquale and Álvaro García-Pérez

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Hutchins' Pure Subtype Systems (PSS) offer a unified framework for types and terms, promising significant advancements in language design for features like dependent types and higher-order subtyping. However, the theory has been hampered by a critical gap: a proof of type safety has remained an open problem for over a decade. The original attempt to prove this property relied on the conjectured commutativity of two fundamental reduction relations, equivalence and subtyping. Proving transitivity elimination, however, requires this commutativity, a property that is notoriously difficult to establish for higher-order subtyping systems. In this paper, we address this issue by introducing Machine-Based PSS (MPSS), a novel reformulation of the original system. MPSS integrates a continuation stack mechanism, reminiscent of the Krivine Abstract Machine, to keep track of arguments that are passed during function application, enabling more fine-grained reductions. This architectural change exposes crucial intermediate reduction steps that were absent in the original PSS. The primary contribution of our work is a direct proof that the equivalence and subtyping reductions in MPSS commute. This result formally establishes transitivity elimination, which is the cornerstone of the inversion lemma required for type safety. We conclude by outlining a pathway from our foundational result to a complete, type-safe system, thereby paving the way for the practical realization of PSS-based languages.
Cite as

Valentin Pasquale and Álvaro García-Pérez. Towards the Type Safety of Pure Subtype Systems. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 37:1-37:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{pasquale_et_al:LIPIcs.CSL.2026.37,
  author =	{Pasquale, Valentin and Garc{\'\i}a-P\'{e}rez, \'{A}lvaro},
  title =	{{Towards the Type Safety of Pure Subtype Systems}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{37:1--37:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.37},
  URN =		{urn:nbn:de:0030-drops-254626},
  doi =		{10.4230/LIPIcs.CSL.2026.37},
  annote =	{Keywords: Lambda calculus, Pure subtype systems, Dependent types, Higher-order subtyping, Type safety}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSCD.2025.1
Computation First: Rebuilding Constructivism with Effects (Invited Talk)

Authors: Liron Cohen

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
Constructive logic and type theory have traditionally been grounded in pure, effect-free model of computation. This paper argues that such a restriction is not a foundational necessity but a historical artifact, and it advocates for a broader perspective of effectful constructivism, where computational effects, such as state, non-determinism, and exceptions, are directly and internally embedded in the logical and computational foundations. We begin by surveying examples where effects reshape logical principles, and then outline three approaches to effectful constructivism, focusing on realizability models: Monadic Combinatory Algebras, which extend classical partial combinatory algebras with effectful computation; Evidenced Frames, a flexible semantic structure capable of uniformly capturing a wide range of effects; and Effectful Higher-Order Logic (EffHOL), a syntactic approach that directly translates logical propositions into specifications for effectful programs. We further illustrate how concrete type theories can internalize effects, via the family of type theories TT^□_C. Together, these works demonstrate that effectful constructivism is not merely possible but a natural and robust extension of traditional frameworks.
Cite as

Liron Cohen. Computation First: Rebuilding Constructivism with Effects (Invited Talk). In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 1:1-1:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cohen:LIPIcs.FSCD.2025.1,
  author =	{Cohen, Liron},
  title =	{{Computation First: Rebuilding Constructivism with Effects}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{1:1--1:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.1},
  URN =		{urn:nbn:de:0030-drops-236167},
  doi =		{10.4230/LIPIcs.FSCD.2025.1},
  annote =	{Keywords: Effectful constructivism, realizability, type theory, monadic combinatory algebras, evidenced frame}
}
Document
Pearl/Brave New Idea
DOI: 10.4230/LIPIcs.ECOOP.2023.41
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.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
Artifact
DOI: 10.4230/DARTS.9.2.13
The Dolorem Pattern: Growing a Language Through Compile-Time Function Execution (Artifact)

Authors: Simon Henniger and Nada Amin

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 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 (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 13:1-13:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{henniger_et_al:DARTS.9.2.13,
  author =	{Henniger, Simon and Amin, Nada},
  title =	{{The Dolorem Pattern: Growing a Language Through Compile-Time Function Execution (Artifact)}},
  pages =	{13:1--13:3},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Henniger, Simon and Amin, Nada},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.13},
  URN =		{urn:nbn:de:0030-drops-182532},
  doi =		{10.4230/DARTS.9.2.13},
  annote =	{Keywords: extensible languages, meta programming, macros, program generation, compilation}
}
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 Type
  • 5 Document/PDF
  • 2 Document/HTML

  • Refine by Publication Year
  • 1 2026
  • 1 2025
  • 2 2023
  • 1 2015

  • Refine by Author
  • 3 Amin, Nada
  • 2 Henniger, Simon
  • 1 Brown, Kevin J.
  • 1 Cohen, Liron
  • 1 Dashti, Mohammad
  • Show More...

  • Refine by Series/Journal
  • 4 LIPIcs
  • 1 DARTS

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

  • Refine by Keyword
  • 2 compilation
  • 2 extensible languages
  • 2 macros
  • 2 meta programming
  • 2 program generation
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact