Formalization and Implementation of Safe Destination Passing in Pure Functional Programming Settings
Universit de Lorraine
AI Insights
- It has two main presentations: monadic and dyadic. [3]
- The monadic presentation, ฮปL1, uses a single context ฮ for both linear and unrestricted variables. [3]
- In contrast, the dyadic presentation, ฮปL2, uses two separate contexts: one for linear variables (ฮ) and another for unrestricted variables (โง). [3]
- Each judgment in ฮปL2 is equipped with a second context โง that holds variable bindings that can be used in an unrestricted fashion. [3]
- The linear lambda calculus (ฮปL) is a formal system that models computation with resources. [2]
- The dyadic presentation of ฮปL2 alleviates the burden of explicit contraction, weakening, and dereliction in the monadic presentation by using two typing contexts. [1]
Abstract
Destination-passing style programming introduces destinations, which represent the address of a write-once memory cell. These destinations can be passed as function parameters, allowing the caller to control memory management: the callee simply fills the cell instead of allocating space for a return value. While typically used in systems programming, destination passing also has applications in pure functional programming, where it enables programs that were previously unexpressible using usual immutable data structures. In this thesis, we develop a core ฮป-calculus with destinations, {ฮป_d}. Our new calculus is more expressive than similar existing systems, with destination passing designed to be as flexible as possible. This is achieved through a modal type system combining linear types with a system of ages to manage scopes, in order to make destination-passing safe. Type safety of our core calculus was proved formally with the Coq proof assistant. Then, we see how this core calculus can be adapted into an existing pure functional language, Haskell, whose type system is less powerful than our custom theoretical one. Retaining safety comes at the cost of removing some flexibility in the handling of destinations. We later refine the implementation to recover much of this flexibility, at the cost of increased user complexity. The prototype implementation in Haskell shows encouraging results for adopting destination-passing style programming when traversing or mapping over large data structures such as lists or data trees.
Destination-passing style programming introduces destinations, which represent the address of a write-once memory cell. These destinations can be passed as function parameters, allowing the caller to control memory management: the callee simply fills the cell instead of allocating space for a return value. While typically used in systems programming, destination passing also has applications in pure functional programming, where it enables programs that were previously unexpressible using usual immutable data structures. In this thesis, we develop a core ฮป-calculus with destinations, {ฮป_d}. Our new calculus is more expressive than similar existing systems, with destination passing designed to be as flexible as possible. This is achieved through a modal type system combining linear types with a system of ages to manage scopes, in order to make destination-passing safe. Type safety of our core calculus was proved formally with the Coq proof assistant. Then, we see how this core calculus can be adapted into an existing pure functional language, Haskell, whose type system is less powerful than our custom theoretical one. Retaining safety comes at the cost of removing some flexibility in the handling of destinations. We later refine the implementation to recover much of this flexibility, at the cost of increased user complexity. The prototype implementation in Haskell shows encouraging results for adopting destination-passing style programming when traversing or mapping over large data structures such as lists or data trees.
Why we are recommending this paper?
Due to your Interest in Functional Programming
This paper directly addresses functional programming, specifically safe destination passing, aligning with your interest in programming paradigms. The focus on pure functional settings provides a relevant context for exploring concepts like memory management and function design.
Due to your Interest in Functional Programming
This paper directly addresses functional programming, specifically safe destination passing, aligning with your interest in programming paradigms. The focus on pure functional settings provides a relevant context for exploring concepts like memory management and function design.
University of Hamburg
AI Insights
- The study aimed to investigate the effectiveness of fun activities in teaching computer science concepts to large classes. [3]
- Both students and educators reported positive experiences with the fun activities, highlighting their ability to increase motivation, engagement, and understanding of complex concepts. [3]
- The main advantages mentioned by both groups were the increased motivation and engagement of students, as well as the help in remembering the content. [3]
- CS-Unplugged: An initiative that collects fun games to teach computer science concepts, primarily for school children. [3]
- Spaghetti Tower: A design game where students use marshmallows and spaghetti to build a tower. [3]
- The study suggests that fun activities can be an effective way to teach computer science concepts, particularly in large classes. [3]
- The study also highlighted potential challenges, such as the need for preparation and time management, as well as cultural differences that may affect the success of these activities. [2]
Abstract
Teaching software development basics to hundreds of students in a frontal setting is cost-efficient and thus still common in universities. However, in a large lecture hall, students can easily get bored, distracted, and disengaged. The frontal setting can also frustrate lecturers since interaction opportunities are limited and hard to scale. Fun activities can activate students and, if well designed, can also help remember and reflect on abstract software development concepts. We present a novel catalogue of ten physical fun activities, developed over years to reflect on basic programming and software development concepts. The catalogue includes the execution of a LA-OLA algorithm as in stadiums, using paper planes to simulate object messages and pointers, and traversing a lecture hall as a tree or a recursive structure. We report our experience of using the activities in a large course with 500+ students three years in a row. We also conducted an interview study with 15 former students of the course and 14 experienced educators from around the globe. The results suggest that the fun activities can enable students to stay focused, remember key concepts, and reflect afterwards. However, keeping the activities concise and clearly linked to the concepts taught seems to be key to their acceptance and effectiveness.
Teaching software development basics to hundreds of students in a frontal setting is cost-efficient and thus still common in universities. However, in a large lecture hall, students can easily get bored, distracted, and disengaged. The frontal setting can also frustrate lecturers since interaction opportunities are limited and hard to scale. Fun activities can activate students and, if well designed, can also help remember and reflect on abstract software development concepts. We present a novel catalogue of ten physical fun activities, developed over years to reflect on basic programming and software development concepts. The catalogue includes the execution of a LA-OLA algorithm as in stadiums, using paper planes to simulate object messages and pointers, and traversing a lecture hall as a tree or a recursive structure. We report our experience of using the activities in a large course with 500+ students three years in a row. We also conducted an interview study with 15 former students of the course and 14 experienced educators from around the globe. The results suggest that the fun activities can enable students to stay focused, remember key concepts, and reflect afterwards. However, keeping the activities concise and clearly linked to the concepts taught seems to be key to their acceptance and effectiveness.
Why we are recommending this paper?
Due to your Interest in Programming Paradigms
Given your interest in programming paradigms and large-scale programming education, this paper offers insights into effective teaching strategies for programming courses. The discussion of engagement and learning techniques is highly pertinent to your area of interest.
Due to your Interest in Programming Paradigms
Given your interest in programming paradigms and large-scale programming education, this paper offers insights into effective teaching strategies for programming courses. The discussion of engagement and learning techniques is highly pertinent to your area of interest.
University of Oxford
AI Insights
- The multi-property winning relation is computed as the least fixed point of the operator F(E) = WinM 0 โช PreMC(E). [2]
- The sequence (WinM i)iโN stabilizes in at most |Sร| ยท2|ฮฆ| steps. [1]
Abstract
We study LTLf synthesis with multiple properties, where satisfying all properties may be impossible. Instead of enumerating subsets of properties, we compute in one fixed-point computation the relation between product-game states and the goal sets that are realizable from them, and we synthesize strategies achieving maximal realizable sets. We develop a fully symbolic algorithm that introduces Boolean goal variables and exploits monotonicity to represent exponentially many goal combinations compactly. Our approach substantially outperforms enumeration-based baselines, with speedups of up to two orders of magnitude.
We study LTLf synthesis with multiple properties, where satisfying all properties may be impossible. Instead of enumerating subsets of properties, we compute in one fixed-point computation the relation between product-game states and the goal sets that are realizable from them, and we synthesize strategies achieving maximal realizable sets. We develop a fully symbolic algorithm that introduces Boolean goal variables and exploits monotonicity to represent exponentially many goal combinations compactly. Our approach substantially outperforms enumeration-based baselines, with speedups of up to two orders of magnitude.
Why we are recommending this paper?
Due to your Interest in Design Patterns
This paper explores synthesizing properties, which is a core concept in formal verification and programming language design. The focus on LTLf synthesis aligns with your interest in rigorous programming and formal methods.
Due to your Interest in Design Patterns
This paper explores synthesizing properties, which is a core concept in formal verification and programming language design. The focus on LTLf synthesis aligns with your interest in rigorous programming and formal methods.
University of Auckland
AI Insights
- The study analyzed 1,036 popular open-source Java repositories on GitHub. [3]
- It found high normalized scores for key categories such as class names, package names, variable names, and private instances, indicating a need for better adherence to code style conventions. [3]
- Selection bias: The study's focus on popular open-source Java repositories may introduce bias, as highly starred repositories may not be representative of the broader ecosystem. [3]
- Repositories that explicitly reference Google's Java Style Guide exhibit the best adherence to programming practice violations. [2]
Abstract
Following code style conventions in software projects is essential for maintaining overall code quality. Adhering to these conventions improves maintainability, understandability, and extensibility. Additionally, following best practices during software development enhances performance and reduces the likelihood of errors. This paper analyzes 1,036 popular open-source JAVA projects on GITHUB to study how code style and programming practices are adopted and evolve over time, examining their prevalence and the most common violations. Additionally, we study a subset of active repositories on a monthly basis to track changes in adherence to coding standards over time. We found widespread violations across repositories, with Javadoc and Naming violations being the most common. We also found a significant number of violations of the GOOGLE Java Style Guide in categories often missed by modern static analysis tools. Furthermore, repositories claiming to follow code-style practices exhibited slightly higher overall adherence to code-style and best-practices. The results provide valuable insights into the adoption of code style and programming practices, highlighting key areas for improvement in the open-source development community. Furthermore, the paper identifies important lessons learned and suggests future directions for improving code quality in JAVA projects.
Following code style conventions in software projects is essential for maintaining overall code quality. Adhering to these conventions improves maintainability, understandability, and extensibility. Additionally, following best practices during software development enhances performance and reduces the likelihood of errors. This paper analyzes 1,036 popular open-source JAVA projects on GITHUB to study how code style and programming practices are adopted and evolve over time, examining their prevalence and the most common violations. Additionally, we study a subset of active repositories on a monthly basis to track changes in adherence to coding standards over time. We found widespread violations across repositories, with Javadoc and Naming violations being the most common. We also found a significant number of violations of the GOOGLE Java Style Guide in categories often missed by modern static analysis tools. Furthermore, repositories claiming to follow code-style practices exhibited slightly higher overall adherence to code-style and best-practices. The results provide valuable insights into the adoption of code style and programming practices, highlighting key areas for improvement in the open-source development community. Furthermore, the paper identifies important lessons learned and suggests future directions for improving code quality in JAVA projects.
Why we are recommending this paper?
Due to your Interest in Programming Paradigms
This paper investigates code style and best practices, directly relating to your interest in programming paradigms and design patterns. Understanding how these practices evolve is crucial for effective software development.
Due to your Interest in Programming Paradigms
This paper investigates code style and best practices, directly relating to your interest in programming paradigms and design patterns. Understanding how these practices evolve is crucial for effective software development.
ETH Zurich
AI Insights
- MLIR-Forge has been used to generate programs for several different IRs, including SDFG, Memref, and Func. [2]
- MLIR-Forge is a modular framework for generating random programs that can be used for testing compiler intermediate representations (IRs). [1]
Abstract
Optimizing compilers are essential for the efficient and correct execution of software across various scientific fields. Domain-specific languages (DSL) typically use higher level intermediate representations (IR) in their compiler pipelines for domain-specific optimizations. As these IRs add to complexity, it is crucial to test them thoroughly. Random program generators have proven to be an effective tool to test compilers through differential and fuzz testing. However, developing specialized program generators for compiler IRs is not straightforward and demands considerable resources. We introduce MLIR-Forge, a novel random program generator framework that leverages the flexibility of MLIR, aiming to simplify the creation of specialized program generators. MLIR-Forge achieves this by splitting the generation process into fundamental building blocks that are language specific, and reusable program creation logic that constructs random programs from these building blocks. This hides complexity and furthermore, even the language specific components can be defined using a set of common tools. We demonstrate MLIR-Forge's capabilities by generating MLIR with built-in dialects, WebAssembly, and a data-centric program representation, DaCe -- requiring less than a week of development time in total for each of them. Using the generated programs we conduct differential testing and find 9 MLIR, 15 WebAssembly, and 774 DaCe groups of bugs with the corresponding program generators, after running them until the rate of new bugs stagnates.
Optimizing compilers are essential for the efficient and correct execution of software across various scientific fields. Domain-specific languages (DSL) typically use higher level intermediate representations (IR) in their compiler pipelines for domain-specific optimizations. As these IRs add to complexity, it is crucial to test them thoroughly. Random program generators have proven to be an effective tool to test compilers through differential and fuzz testing. However, developing specialized program generators for compiler IRs is not straightforward and demands considerable resources. We introduce MLIR-Forge, a novel random program generator framework that leverages the flexibility of MLIR, aiming to simplify the creation of specialized program generators. MLIR-Forge achieves this by splitting the generation process into fundamental building blocks that are language specific, and reusable program creation logic that constructs random programs from these building blocks. This hides complexity and furthermore, even the language specific components can be defined using a set of common tools. We demonstrate MLIR-Forge's capabilities by generating MLIR with built-in dialects, WebAssembly, and a data-centric program representation, DaCe -- requiring less than a week of development time in total for each of them. Using the generated programs we conduct differential testing and find 9 MLIR, 15 WebAssembly, and 774 DaCe groups of bugs with the corresponding program generators, after running them until the rate of new bugs stagnates.
Why we are recommending this paper?
Due to your Interest in Programming Language Design
This paper explores compiler design and optimization, particularly using intermediate representations, which is relevant to programming language design and performance. The focus on DSLs aligns with a deeper understanding of language structure.
Due to your Interest in Programming Language Design
This paper explores compiler design and optimization, particularly using intermediate representations, which is relevant to programming language design and performance. The focus on DSLs aligns with a deeper understanding of language structure.
Stockholm University
AI Insights
- The authors acknowledge support from the Research Council of Norway, grant numbers 288761 and 326537. [3]
- OBDD: Ordered Binary Decision Diagram bB(w): The set of all OBDDs with width at most w bB(w) โ: The set of all OBDDs with width at most w and length at most n L(D): The language accepted by the OBDD D Functional Decomposition: Given an OBDD D, determine whether there exist OBDDs D_1,...,D_k such that L(D) = L(D_1) โฉ ... [3]
- The paper introduces a new framework for addressing functional reconfiguration and decomposition problems using techniques from automata theory and parameterized complexity theory. [2]
- โฉ L(D_k) Functional Reconfiguration: Given an OBDD D and a target OBDD T, determine whether it is possible to reconfigure D into T [1]
Abstract
Functional decomposition is the process of breaking down a function $f$ into a composition $f=g(f_1,\dots,f_k)$ of simpler functions $f_1,\dots,f_k$ belonging to some class $\mathcal{F}$. This fundamental notion can be used to model applications arising in a wide variety of contexts, ranging from machine learning to formal language theory. In this work, we study functional decomposition by leveraging on the notion of functional reconfiguration. In this setting, constraints are imposed not only on the factor functions $f_1,\dots,f_k$ but also on the intermediate functions arising during the composition process. We introduce a symbolic framework to address functional reconfiguration and decomposition problems. In our framework, functions arising during the reconfiguration process are represented symbolically, using ordered binary decision diagrams (OBDDs). The function $g$ used to specify the reconfiguration process is represented by a Boolean circuit $C$. Finally, the function class $\mathcal{F}$ is represented by a second-order finite automaton $\mathcal{A}$. Our main result states that functional reconfiguration, and hence functional decomposition, can be solved in fixed-parameter linear time when parameterized by the width of the input OBDD, by structural parameters associated with the reconfiguration circuit $C$, and by the size of the second-order finite automaton $\mathcal{A}$.
Functional decomposition is the process of breaking down a function $f$ into a composition $f=g(f_1,\dots,f_k)$ of simpler functions $f_1,\dots,f_k$ belonging to some class $\mathcal{F}$. This fundamental notion can be used to model applications arising in a wide variety of contexts, ranging from machine learning to formal language theory. In this work, we study functional decomposition by leveraging on the notion of functional reconfiguration. In this setting, constraints are imposed not only on the factor functions $f_1,\dots,f_k$ but also on the intermediate functions arising during the composition process. We introduce a symbolic framework to address functional reconfiguration and decomposition problems. In our framework, functions arising during the reconfiguration process are represented symbolically, using ordered binary decision diagrams (OBDDs). The function $g$ used to specify the reconfiguration process is represented by a Boolean circuit $C$. Finally, the function class $\mathcal{F}$ is represented by a second-order finite automaton $\mathcal{A}$. Our main result states that functional reconfiguration, and hence functional decomposition, can be solved in fixed-parameter linear time when parameterized by the width of the input OBDD, by structural parameters associated with the reconfiguration circuit $C$, and by the size of the second-order finite automaton $\mathcal{A}$.
Why we are recommending this paper?
Due to your Interest in Functional Programming
Due to your Interest in Functional Programming
Interests not found
We did not find any papers that match the below interests.
Try other terms also consider if the content exists in arxiv.org.
- Object Oriented Programming
You can edit or add more interests any time.
๐ฌ Help Shape Our Pricing
We're exploring pricing options to make this project sustainable. Take 3 minutes to share what you'd be willing to pay (if anything). Your input guides our future investment.
Help us improve your experience!
This project is on its early stages your feedback can be pivotal on the future of the project.
Let us know what you think about this week's papers and suggestions!
Give Feedback