28 Search Results for "Chung, Benjamin"

Document
DOI: 10.4230/OASIcs.ICPEC.2024.18
Using ChatGPT During Implementation of Programs in Education

Authors: Norbert Baláž, Jaroslav Porubän, Marek Horváth, and Tomáš Kormaník

Published in: OASIcs, Volume 122, 5th International Computer Programming Education Conference (ICPEC 2024)

Abstract
This paper examines the impact of ChatGPT on programming education by conducting an empirical study with computer science students at the Department of Computers and Informatics at the Technical University in Košice. The study involves an experiment where students in a Component Programming course use ChatGPT to solve a programming task involving linked lists, comparing their performance and understanding with a control group that does not use the AI (artificial intelligence) tool. The task necessitated the implementation of a function to add two numbers represented as linked lists in reverse order. Our findings indicate that while ChatGPT significantly enhances the speed of task completion - students using it were nearly three times quicker on average - it may also detract from deep understanding and critical thinking, as evidenced by the uniformity and superficial engagement in solutions among the ChatGPT group. On the other hand, the group working independently displayed a broader variety of solutions and deeper interaction with the problem, despite slower completion times and occasional inaccuracies. The results highlight a dual-edged impact of AI tools in education: while they enhance efficiency, they may undermine the development of critical thinking and problem-solving skills. We discuss the implications of these findings for educational practices, emphasizing the need for a balanced approach that integrates AI tools without compromising the depth of learning and understanding in students.
Cite as

Norbert Baláž, Jaroslav Porubän, Marek Horváth, and Tomáš Kormaník. Using ChatGPT During Implementation of Programs in Education. In 5th International Computer Programming Education Conference (ICPEC 2024). Open Access Series in Informatics (OASIcs), Volume 122, pp. 18:1-18:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{balaz_et_al:OASIcs.ICPEC.2024.18,
  author =	{Bal\'{a}\v{z}, Norbert and Porub\"{a}n, Jaroslav and Horv\'{a}th, Marek and Korman{\'\i}k, Tom\'{a}\v{s}},
  title =	{{Using ChatGPT During Implementation of Programs in Education}},
  booktitle =	{5th International Computer Programming Education Conference (ICPEC 2024)},
  pages =	{18:1--18:9},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-347-8},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{122},
  editor =	{Santos, Andr\'{e} L. and Pinto-Albuquerque, Maria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICPEC.2024.18},
  URN =		{urn:nbn:de:0030-drops-209876},
  doi =		{10.4230/OASIcs.ICPEC.2024.18},
  annote =	{Keywords: generative artificial intelligence, chatbot, ChatGPT, prompt engineering, source code generation}
}
Document
DOI: 10.4230/LIPIcs.ESA.2024.37
Online Flexible Busy Time Scheduling on Heterogeneous Machines

Authors: Gruia Călinescu, Sami Davies, Samir Khuller, and Shirley Zhang

Published in: LIPIcs, Volume 308, 32nd Annual European Symposium on Algorithms (ESA 2024)

Abstract
We study the online busy time scheduling model on heterogeneous machines. In our setting, jobs with uniform length arrive online with a deadline that becomes known to the algorithm at the job’s arrival time. An algorithm has access to machines, each with different associated capacities and costs. The goal is to schedule jobs on machines by their deadline, so that the total cost incurred by the scheduling algorithm is minimized. While busy time scheduling has been well-studied, relatively little is known when machines are heterogeneous (i.e., have different costs and capacities), despite this natural theoretical generalization being the most practical model for clients using cloud computing services. We make significant progress in understanding this model by designing an 8-competitive algorithm for the problem on unit-length jobs and provide a lower bound of 2 on the competitive ratio. The lower bound is tight in the setting when jobs form non-nested intervals. Our 8-competitive algorithm generalizes to one with competitive ratio 8(2p-1)/p < 16 when all jobs have uniform length p.
Cite as

Gruia Călinescu, Sami Davies, Samir Khuller, and Shirley Zhang. Online Flexible Busy Time Scheduling on Heterogeneous Machines. In 32nd Annual European Symposium on Algorithms (ESA 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 308, pp. 37:1-37:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{calinescu_et_al:LIPIcs.ESA.2024.37,
  author =	{C\u{a}linescu, Gruia and Davies, Sami and Khuller, Samir and Zhang, Shirley},
  title =	{{Online Flexible Busy Time Scheduling on Heterogeneous Machines}},
  booktitle =	{32nd Annual European Symposium on Algorithms (ESA 2024)},
  pages =	{37:1--37:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-338-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{308},
  editor =	{Chan, Timothy and Fischer, Johannes and Iacono, John and Herman, Grzegorz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ESA.2024.37},
  URN =		{urn:nbn:de:0030-drops-211083},
  doi =		{10.4230/LIPIcs.ESA.2024.37},
  annote =	{Keywords: Online algorithms, Scheduling, Competitive analysis}
}
Document
APPROX
DOI: 10.4230/LIPIcs.APPROX/RANDOM.2024.2
Online Time-Windows TSP with Predictions

Authors: Shuchi Chawla and Dimitris Christou

Published in: LIPIcs, Volume 317, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2024)

Abstract
In the Time-Windows TSP (TW-TSP) we are given requests at different locations on a network; each request is endowed with a reward and an interval of time; the goal is to find a tour that visits as much reward as possible during the corresponding time window. For the online version of this problem, where each request is revealed at the start of its time window, no finite competitive ratio can be obtained. We consider a version of the problem where the algorithm is presented with predictions of where and when the online requests will appear, without any knowledge of the quality of this side information. Vehicle routing problems such as the TW-TSP can be very sensitive to errors or changes in the input due to the hard time-window constraints, and it is unclear whether imperfect predictions can be used to obtain a finite competitive ratio. We show that good performance can be achieved by explicitly building slack into the solution. Our main result is an online algorithm that achieves a competitive ratio logarithmic in the diameter of the underlying network, matching the performance of the best offline algorithm to within factors that depend on the quality of the provided predictions. The competitive ratio degrades smoothly as a function of the quality and we show that this dependence is tight within constant factors.
Cite as

Shuchi Chawla and Dimitris Christou. Online Time-Windows TSP with Predictions. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 317, pp. 2:1-2:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{chawla_et_al:LIPIcs.APPROX/RANDOM.2024.2,
  author =	{Chawla, Shuchi and Christou, Dimitris},
  title =	{{Online Time-Windows TSP with Predictions}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2024)},
  pages =	{2:1--2:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-348-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{317},
  editor =	{Kumar, Amit and Ron-Zewi, Noga},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2024.2},
  URN =		{urn:nbn:de:0030-drops-209954},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2024.2},
  annote =	{Keywords: Travelling Salesman Problem, Predictions, Learning-Augmented Algorithms, Approximation}
}
Document
APPROX
DOI: 10.4230/LIPIcs.APPROX/RANDOM.2024.5
Asynchronous Majority Dynamics on Binomial Random Graphs

Authors: Divyarthi Mohan and Paweł Prałat

Published in: LIPIcs, Volume 317, Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2024)

Abstract
We study information aggregation in networks when agents interact to learn a binary state of the world. Initially each agent privately observes an independent signal which is correct with probability 1/2+δ for some δ > 0. At each round, a node is selected uniformly at random to update their public opinion to match the majority of their neighbours (breaking ties in favour of their initial private signal). Our main result shows that for sparse and connected binomial random graphs G(n,p) the process stabilizes in a correct consensus in 𝒪(nlog² n/log log n) steps with high probability. In fact, when log n/n ≪ p = o(1) the process terminates at time T^ = (1+o(1))nlog n, where T^ is the first time when all nodes have been selected at least once. However, in dense binomial random graphs with p = Ω(1), there is an information cascade where the process terminates in the incorrect consensus with probability bounded away from zero.
Cite as

Divyarthi Mohan and Paweł Prałat. Asynchronous Majority Dynamics on Binomial Random Graphs. In Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 317, pp. 5:1-5:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{mohan_et_al:LIPIcs.APPROX/RANDOM.2024.5,
  author =	{Mohan, Divyarthi and Pra{\l}at, Pawe{\l}},
  title =	{{Asynchronous Majority Dynamics on Binomial Random Graphs}},
  booktitle =	{Approximation, Randomization, and Combinatorial Optimization. Algorithms and Techniques (APPROX/RANDOM 2024)},
  pages =	{5:1--5:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-348-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{317},
  editor =	{Kumar, Amit and Ron-Zewi, Noga},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.APPROX/RANDOM.2024.5},
  URN =		{urn:nbn:de:0030-drops-209985},
  doi =		{10.4230/LIPIcs.APPROX/RANDOM.2024.5},
  annote =	{Keywords: Opinion dynamics, Social learning, Stochastic processes, Random Graphs, Consensus}
}
Document
DOI: 10.4230/LIPIcs.AFT.2024.9
Blockchain Space Tokenization

Authors: Aggelos Kiayias, Elias Koutsoupias, Philip Lazos, and Giorgos Panagiotakos

Published in: LIPIcs, Volume 316, 6th Conference on Advances in Financial Technologies (AFT 2024)

Abstract
Handling congestion in blockchain systems is a fundamental problem given that the security and decentralization objectives of such systems lead to designs that compromise on (horizontal) scalability (what sometimes is referred to as the "blockchain trilemma"). Motivated by this, we focus on the question whether it is possible to design a transaction inclusion policy for block producers that facilitates fee and delay predictability while being incentive compatible at the same time. Reconciling these three properties is seemingly paradoxical given that the dominant approach to transaction processing is based on first-price auctions (e.g., as in Bitcoin) or dynamic adjustment of the minimum admissible fee (e.g. as in Ethereum EIP-1559) something that breaks fee predictability. At the same time, in fixed fee mechanisms (e.g., as in Cardano), fees are trivially predictable but are subject to relatively inexpensive bribing or denial of service attacks where transactions may be delayed indefinitely by a well funded attacker, hence breaking delay predictability. In this work, we set out to address this problem by putting forward blockchain space tokenization (BST), namely a new capability of a blockchain system to tokenize its capacity for transactions and allocate it to interested users who are willing to pay ahead of time for the ability to post transactions regularly for a period of time. We analyze our system in the face of worst-case transaction-processing attacks by introducing a security game played between the mempool mechanism and an adversary. Leveraging this framework, we prove that BST offers predictable and asymptotically optimal delays, predictable fees, and is incentive compatible, thus answering the question posed in the affirmative.
Cite as

Aggelos Kiayias, Elias Koutsoupias, Philip Lazos, and Giorgos Panagiotakos. Blockchain Space Tokenization. In 6th Conference on Advances in Financial Technologies (AFT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 316, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{kiayias_et_al:LIPIcs.AFT.2024.9,
  author =	{Kiayias, Aggelos and Koutsoupias, Elias and Lazos, Philip and Panagiotakos, Giorgos},
  title =	{{Blockchain Space Tokenization}},
  booktitle =	{6th Conference on Advances in Financial Technologies (AFT 2024)},
  pages =	{9:1--9:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-345-4},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{316},
  editor =	{B\"{o}hme, Rainer and Kiffer, Lucianna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2024.9},
  URN =		{urn:nbn:de:0030-drops-209453},
  doi =		{10.4230/LIPIcs.AFT.2024.9},
  annote =	{Keywords: Blockchain protocols, Predictable Service, Transaction Fees}
}
Document
DOI: 10.4230/LIPIcs.AFT.2024.11
Bribe & Fork: Cheap PCN Bribing Attacks via Forking Threat

Authors: Zeta Avarikioti, Paweł Kędzior, Tomasz Lizurej, and Tomasz Michalak

Published in: LIPIcs, Volume 316, 6th Conference on Advances in Financial Technologies (AFT 2024)

Abstract
In this work, we reexamine the vulnerability of Payment Channel Networks (PCNs) to bribing attacks, where an adversary incentivizes blockchain miners to deliberately ignore a specific transaction to undermine the punishment mechanism of PCNs. While previous studies have posited a prohibitive cost for such attacks, we show that this cost can be dramatically reduced (to approximately $125), thereby increasing the likelihood of these attacks. To this end, we introduce Bribe & Fork, a modified bribing attack that leverages the threat of a so-called feather fork which we analyze with a novel formal model for the mining game with forking. We empirically analyze historical data of some real-world blockchain implementations to evaluate the scale of this cost reduction. Our findings shed more light on the potential vulnerability of PCNs and highlight the need for robust solutions.
Cite as

Zeta Avarikioti, Paweł Kędzior, Tomasz Lizurej, and Tomasz Michalak. Bribe & Fork: Cheap PCN Bribing Attacks via Forking Threat. In 6th Conference on Advances in Financial Technologies (AFT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 316, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{avarikioti_et_al:LIPIcs.AFT.2024.11,
  author =	{Avarikioti, Zeta and K\k{e}dzior, Pawe{\l} and Lizurej, Tomasz and Michalak, Tomasz},
  title =	{{Bribe \& Fork: Cheap PCN Bribing Attacks via Forking Threat}},
  booktitle =	{6th Conference on Advances in Financial Technologies (AFT 2024)},
  pages =	{11:1--11:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-345-4},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{316},
  editor =	{B\"{o}hme, Rainer and Kiffer, Lucianna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2024.11},
  URN =		{urn:nbn:de:0030-drops-209473},
  doi =		{10.4230/LIPIcs.AFT.2024.11},
  annote =	{Keywords: Blockchain, Payment Channels Networks, Timelock Bribing, Feather Forking}
}
Document
DOI: 10.4230/LIPIcs.AFT.2024.29
Transaction Fee Mechanism Design in a Post-MEV World

Authors: Maryam Bahrani, Pranav Garimidi, and Tim Roughgarden

Published in: LIPIcs, Volume 316, 6th Conference on Advances in Financial Technologies (AFT 2024)

Abstract
The incentive-compatibility properties of blockchain transaction fee mechanisms have been investigated with passive block producers that are motivated purely by the net rewards earned at the consensus layer. This paper introduces a model of active block producers that have their own private valuations for blocks (representing, for example, additional value derived from the application layer). The block producer surplus in our model can be interpreted as one of the more common colloquial meanings of the phrase "maximal extractable value (MEV)." We first prove that transaction fee mechanism design is fundamentally more difficult with active block producers than with passive ones: With active block producers, no non-trivial or approximately welfare-maximizing transaction fee mechanism can be incentive-compatible for both users and block producers. These results can be interpreted as a mathematical justification for augmenting transaction fee mechanisms with additional components such as order flow auctions, block producer competition, trusted hardware, or cryptographic techniques. We then consider a more fine-grained model of block production that more accurately reflects current practice, in which we distinguish the roles of "searchers" (who actively identify opportunities for value extraction from the application layer and compete for the right to take advantage of them) and "proposers" (who participate directly in the blockchain protocol and make the final choice of the published block). Searchers can effectively act as an "MEV oracle" for a transaction fee mechanism, thereby enlarging the design space. Here, we first consider a TFM that is inspired by how searchers have traditionally been incorporated into the block production process, with each transaction effectively sold off to a searcher through a first-price auction. We then explore the TFM design space with searchers more generally, and design a mechanism that circumvents our impossibility results for TFMs without searchers. Our mechanism (the "SAKA" mechanism) is incentive-compatible (for users, searchers, and the block producer), sybil-proof, and guarantees roughly 50% of the maximum-possible welfare when transaction sizes are small relative to block sizes. We conclude with a matching negative result: even when transaction sizes are small, no DSIC and sybil-proof deterministic TFM can guarantee more than 50% of the maximum-possible welfare.
Cite as

Maryam Bahrani, Pranav Garimidi, and Tim Roughgarden. Transaction Fee Mechanism Design in a Post-MEV World. In 6th Conference on Advances in Financial Technologies (AFT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 316, pp. 29:1-29:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bahrani_et_al:LIPIcs.AFT.2024.29,
  author =	{Bahrani, Maryam and Garimidi, Pranav and Roughgarden, Tim},
  title =	{{Transaction Fee Mechanism Design in a Post-MEV World}},
  booktitle =	{6th Conference on Advances in Financial Technologies (AFT 2024)},
  pages =	{29:1--29:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-345-4},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{316},
  editor =	{B\"{o}hme, Rainer and Kiffer, Lucianna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2024.29},
  URN =		{urn:nbn:de:0030-drops-209658},
  doi =		{10.4230/LIPIcs.AFT.2024.29},
  annote =	{Keywords: MEV, Transaction Fee Mechanisms, Auctions}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.28
Static Basic Block Versioning

Authors: Olivier Melançon, Marc Feeley, and Manuel Serrano

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

Abstract
Basic Block Versioning (BBV) is a compilation technique for optimizing program execution. It consists in duplicating and specializing basic blocks of code according to the execution contexts of the blocks, up to a version limit. BBV has been used in Just-In-Time (JIT) compilers for reducing the dynamic type checks of dynamic languages. Our work revisits the BBV technique to adapt it to Ahead-of-Time (AOT) compilation. This Static BBV (SBBV) raises new challenges, most importantly how to ensure the convergence of the algorithm when the specializations of the basic blocks are not based on profiled variable values and how to select the good specialization contexts. SBBV opens new opportunities for more precise optimizations as the compiler can explore multiple versions and only keep those within the version limit that yield better generated code. In this paper, we present the main SBBV algorithm and its use to optimize the dynamic type checks, array bound checks, and mixed-type arithmetic operators often found in dynamic languages. We have implemented SBBV in two AOT compilers for the Scheme programming language that we have used to evaluate the technique’s effectiveness. On a suite of benchmarks, we have observed that even with a low limit of 2 versions, SBBV greatly reduces the number of dynamic type tests (by 54% and 62% on average) and accelerates the execution time (by about 10% on average). Previous work has needed a higher version limit to achieve a similar level of optimization. We also observe a small impact on compilation time and code size (a decrease in some cases).
Cite as

Olivier Melançon, Marc Feeley, and Manuel Serrano. Static Basic Block Versioning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 28:1-28:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{melancon_et_al:LIPIcs.ECOOP.2024.28,
  author =	{Melan\c{c}on, Olivier and Feeley, Marc and Serrano, Manuel},
  title =	{{Static Basic Block Versioning}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{28:1--28:27},
  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.28},
  URN =		{urn:nbn:de:0030-drops-208770},
  doi =		{10.4230/LIPIcs.ECOOP.2024.28},
  annote =	{Keywords: Compiler, Ahead-of-Time Compilation, Optimization, Dynamic Languages}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.39
Formalizing, Mechanizing, and Verifying Class-Based Refinement Types

Authors: Ke Sun, Di Wang, Sheng Chen, Meng Wang, and Dan Hao

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

Abstract
Refinement types have been extensively used in class-based languages to specify and verify fine-grained logical specifications. Despite the advances in practical aspects such as applicability and usability, two fundamental issues persist. First, the soundness of existing class-based refinement type systems is inadequately explored, casting doubts on their reliability. Second, the expressiveness of existing systems is limited, restricting the depiction of semantic properties related to object-oriented constructs. This work tackles these issues through a systematic framework. We formalize a declarative class-based refinement type calculus (named RFJ), that is expressive and concise. We rigorously develop the soundness meta-theory of this calculus, followed by its mechanization in Coq. Finally, to ensure the calculus’s verifiability, we propose an algorithmic verification approach based on a fragment of first-order logic (named LFJ), and implement this approach as a type checker.
Cite as

Ke Sun, Di Wang, Sheng Chen, Meng Wang, and Dan Hao. Formalizing, Mechanizing, and Verifying Class-Based Refinement Types. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 39:1-39:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{sun_et_al:LIPIcs.ECOOP.2024.39,
  author =	{Sun, Ke and Wang, Di and Chen, Sheng and Wang, Meng and Hao, Dan},
  title =	{{Formalizing, Mechanizing, and Verifying Class-Based Refinement Types}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{39:1--39:30},
  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.39},
  URN =		{urn:nbn:de:0030-drops-208881},
  doi =		{10.4230/LIPIcs.ECOOP.2024.39},
  annote =	{Keywords: Refinement Types, Program Verification, Object-oriented Programming}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.40
Information Flow Control in Cyclic Process Networks

Authors: Bas van den Heuvel, Farzaneh Derakhshan, and Stephanie Balzer

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

Abstract
Protection of confidential data is an important security consideration of today’s applications. Of particular concern is to guard against unintentional leakage to a (malicious) observer, who may interact with the program and draw inference from made observations. Information flow control (IFC) type systems address this concern by statically ruling out such leakage. This paper contributes an IFC type system for message-passing concurrent programs, the computational model of choice for many of today’s applications such as cloud computing and IoT applications. Such applications typically either implicitly or explicitly codify protocols according to which message exchange must happen, and to statically ensure protocol safety, behavioral type systems such as session types can be used. This paper marries IFC with session typing and contributes over prior work in the following regards: (1) support of realistic cyclic process networks as opposed to the restriction to tree-shaped networks, (2) more permissive, yet entirely secure, IFC control, exploiting cyclic process networks, and (3) considering deadlocks as another form of side channel, and asserting deadlock-sensitive noninterference (DSNI) for well-typed programs. To prove DSNI, the paper develops a novel logical relation that accounts for cyclic process networks. The logical relation is rooted in linear logic, but drops the tree-topology restriction imposed by prior work.
Cite as

Bas van den Heuvel, Farzaneh Derakhshan, and Stephanie Balzer. Information Flow Control in Cyclic Process Networks. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 40:1-40:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{vandenheuvel_et_al:LIPIcs.ECOOP.2024.40,
  author =	{van den Heuvel, Bas and Derakhshan, Farzaneh and Balzer, Stephanie},
  title =	{{Information Flow Control in Cyclic Process Networks}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{40:1--40:30},
  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.40},
  URN =		{urn:nbn:de:0030-drops-208891},
  doi =		{10.4230/LIPIcs.ECOOP.2024.40},
  annote =	{Keywords: Cyclic process networks, linear session types, logical relations, deadlock-sensitive noninterference}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.44
Type Tailoring

Authors: Ashton Wiersdorf, Stephen Chang, Matthias Felleisen, and Ben Greenman

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

Abstract
Type systems evolve too slowly to keep up with the quick evolution of libraries - especially libraries that introduce abstractions. Type tailoring offers a lightweight solution by equipping the core language with an API for modifying the elaboration of surface code into the internal language of the typechecker. Through user-programmable elaboration, tailoring rules appear to improve the precision and expressiveness of the underlying type system. Furthermore, type tailoring cooperates with the host type system by expanding to code that the host then typechecks. In the context of a hygienic metaprogramming system, tailoring rules can even harmoniously compose with one another. Type tailoring has emerged as a theme across several languages and metaprogramming systems, but never with direct support and rarely in the same shape twice. For example, both OCaml and Typed Racket enable forms of tailoring, but in quite different ways. This paper identifies key dimensions of type tailoring systems and tradeoffs along each dimension. It demonstrates the usefulness of tailoring with examples that cover sized vectors, database queries, and optional types. Finally, it outlines a vision for future research at the intersection of types and metaprogramming.
Cite as

Ashton Wiersdorf, Stephen Chang, Matthias Felleisen, and Ben Greenman. Type Tailoring. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 44:1-44:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{wiersdorf_et_al:LIPIcs.ECOOP.2024.44,
  author =	{Wiersdorf, Ashton and Chang, Stephen and Felleisen, Matthias and Greenman, Ben},
  title =	{{Type Tailoring}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{44:1--44:27},
  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.44},
  URN =		{urn:nbn:de:0030-drops-208933},
  doi =		{10.4230/LIPIcs.ECOOP.2024.44},
  annote =	{Keywords: Types, Metaprogramming, Macros, Partial Evaluation}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.COSIT.2024.24
Towards a General Framework for Co-Location (Short Paper)

Authors: Keiran Suchak and Ed Manley

Published in: LIPIcs, Volume 315, 16th International Conference on Spatial Information Theory (COSIT 2024)

Abstract
Previous studies into co-location exist in a variety of fields such as epidemiology and human mobility. In each field, researchers are interested identifying points of co-location amongst members of a population. In each of these fields, however, the definition of what it means for members of the population to be co-located may differ; furthermore, the ways in which data are collected vary. This piece of work aims to provide an initial outline of a general framework for identifying points of co-location. It demonstrates that the identification of co-location points between individuals is sensitive to the way in which co-location is defined in each context, as well as the types of data used. Furthermore, it highlights the impact that uncertainty in observations can have on our ability to reliably identify co-location.
Cite as

Keiran Suchak and Ed Manley. Towards a General Framework for Co-Location (Short Paper). In 16th International Conference on Spatial Information Theory (COSIT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 315, pp. 24:1-24:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{suchak_et_al:LIPIcs.COSIT.2024.24,
  author =	{Suchak, Keiran and Manley, Ed},
  title =	{{Towards a General Framework for Co-Location}},
  booktitle =	{16th International Conference on Spatial Information Theory (COSIT 2024)},
  pages =	{24:1--24:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-330-0},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{315},
  editor =	{Adams, Benjamin and Griffin, Amy L. and Scheider, Simon and McKenzie, Grant},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.COSIT.2024.24},
  URN =		{urn:nbn:de:0030-drops-208391},
  doi =		{10.4230/LIPIcs.COSIT.2024.24},
  annote =	{Keywords: human mobility, co-location, contact tracing}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.9
Verifying Peephole Rewriting in SSA Compiler IRs

Authors: Siddharth Bhat, Alex Keizer, Chris Hughes, Andrés Goens, and Tobias Grosser

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
There is an increasing need for domain-specific reasoning in modern compilers. This has fueled the use of tailored intermediate representations (IRs) based on static single assignment (SSA), like in the MLIR compiler framework. Interactive theorem provers (ITPs) provide strong guarantees for the end-to-end verification of compilers (e.g., CompCert). However, modern compilers and their IRs evolve at a rate that makes proof engineering alongside them prohibitively expensive. Nevertheless, well-scoped push-button automated verification tools such as the Alive peephole verifier for LLVM-IR gained recognition in domains where SMT solvers offer efficient (semi) decision procedures. In this paper, we aim to combine the convenience of automation with the versatility of ITPs for verifying peephole rewrites across domain-specific IRs. We formalize a core calculus for SSA-based IRs that is generic over the IR and covers so-called regions (nested scoping used by many domain-specific IRs in the MLIR ecosystem). Our mechanization in the Lean proof assistant provides a user-friendly frontend for translating MLIR syntax into our calculus. We provide scaffolding for defining and verifying peephole rewrites, offering tactics to eliminate the abstraction overhead of our SSA calculus. We prove correctness theorems about peephole rewriting, as well as two classical program transformations. To evaluate our framework, we consider three use cases from the MLIR ecosystem that cover different levels of abstractions: (1) bitvector rewrites from LLVM, (2) structured control flow, and (3) fully homomorphic encryption. We envision that our mechanization provides a foundation for formally verified rewrites on new domain-specific IRs.
Cite as

Siddharth Bhat, Alex Keizer, Chris Hughes, Andrés Goens, and Tobias Grosser. Verifying Peephole Rewriting in SSA Compiler IRs. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 9:1-9:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bhat_et_al:LIPIcs.ITP.2024.9,
  author =	{Bhat, Siddharth and Keizer, Alex and Hughes, Chris and Goens, Andr\'{e}s and Grosser, Tobias},
  title =	{{Verifying Peephole Rewriting in SSA Compiler IRs}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{9:1--9:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.9},
  URN =		{urn:nbn:de:0030-drops-207372},
  doi =		{10.4230/LIPIcs.ITP.2024.9},
  annote =	{Keywords: compilers, semantics, mechanization, MLIR, SSA, regions, peephole rewrites}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.32
Abstractions for Multi-Sorted Substitutions

Authors: Hannes Saffrich

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
Formalizing a typed programming language in a proof assistant requires to choose representations for variables and typing. Variables are often represented as de Bruijn indices, where substitution is usually defined in terms of renamings to allow for proofs by structural induction. Typing can be represented extrinsically by defining untyped terms and a typing relation, or intrinsically by combining syntax and typing into a single definition of well-typed terms. For extrinsic typing, there is again a choice between extrinsic scoping, where terms and the notion of free variables are defined separately, and intrinsic scoping, where terms are indexed by their free variables. This paper describes an Agda framework for formalizing programming languages with extrinsic typing, intrinsic scoping, and de Bruijn Indices for variables. The framework supports object languages with arbitrary many variable sorts and dependencies, making it suitable for polymorphic languages and dependent types. Given an Agda definition of syntax and typing, the framework derives substitution operations and lemmas for untyped terms, and provides an abstraction to prove type preservation of these operations with just a single lemma. The key insights behind the framework are the use of multi-sorted syntax definitions, which enable parallel substitutions that replace all variables of all sorts simultaneously, and abstractions that unify the definitions, compositions, typings, and type preservation lemmas of multi-sorted renamings and substitutions. Case studies have been conducted to prove subject reduction for System F with subtyping, dependently typed lambda calculus, and lambda calculus with pattern matching.
Cite as

Hannes Saffrich. Abstractions for Multi-Sorted Substitutions. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{saffrich:LIPIcs.ITP.2024.32,
  author =	{Saffrich, Hannes},
  title =	{{Abstractions for Multi-Sorted Substitutions}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{32:1--32:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.32},
  URN =		{urn:nbn:de:0030-drops-207609},
  doi =		{10.4230/LIPIcs.ITP.2024.32},
  annote =	{Keywords: Agda, Metatheory, Framework}
}
Document
DOI: 10.4230/LIPIcs.ITP.2024.36
Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model

Authors: Andrew Tolmach, Chris Chhak, and Sean Anderson

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
We propose a concrete ("pointer as integer") memory semantics for C that supports verified compilation to a target environment having simple "public vs. private" data protection based on tagging or sandboxing (such as the WebAssembly virtual machine). Our semantics gives definition to a range of legacy programming idioms that cause undefined behavior in standard C, and are not covered by existing verified compilers, but that often work in practice. Compiler correctness in this context implies that target programs are secure against all control-flow attacks (although not against data-only attacks). To avoid tying our semantics too closely to particular compiler implementation choices, it is parameterized by a novel form of oracle that non-deterministically chooses the addresses of stack and heap allocations. As a proof-of-concept, we formalize a small RTL-like language and verify two-way refinement for a compiler from this language to a low-level machine and runtime system with hardware tagging. Our Coq formalization and proofs are provided as supplementary material.
Cite as

Andrew Tolmach, Chris Chhak, and Sean Anderson. Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 36:1-36:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{tolmach_et_al:LIPIcs.ITP.2024.36,
  author =	{Tolmach, Andrew and Chhak, Chris and Anderson, Sean},
  title =	{{Defining and Preserving More C Behaviors: Verified Compilation Using a Concrete Memory Model}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{36:1--36:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.36},
  URN =		{urn:nbn:de:0030-drops-207643},
  doi =		{10.4230/LIPIcs.ITP.2024.36},
  annote =	{Keywords: Compiler verification, C language semantics, Coq proof assistant}
}
  • Refine by Author
  • 5 Chung, Benjamin
  • 4 Vitek, Jan
  • 2 Li, Paley
  • 2 Meeks, Kitty
  • 2 Nardelli, Francesco Zappa
  • Show More...

  • Refine by Classification
  • 5 Theory of computation → Type theory
  • 3 Mathematics of computing → Graph algorithms
  • 3 Software and its engineering → Semantics
  • 2 Security and privacy → Distributed systems security
  • 2 Security and privacy → Logic and verification
  • Show More...

  • Refine by Keyword
  • 2 Gradual typing
  • 2 Type systems
  • 2 language design
  • 2 object-orientation
  • 2 type systems
  • Show More...

  • Refine by Type
  • 28 document

  • Refine by Publication Year
  • 22 2024
  • 2 2018
  • 2 2019
  • 1 2015
  • 1 2022

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