Programming Languages
A community of developers has formed to modernize the Fortran ecosystem. In this article, we describe the high-level features of Fortran that continue to make it a good choice for scientists and engineers in the 21st century. Ongoing…
A growing body of research on probabilistic programs and causal models has highlighted the need to reason compositionally about model classes that extend directed graphical models. Both probabilistic programs and causal models define a…
Ordinals can help prove termination for dependently typed programs. Brouwer trees are a particular ordinal notation that make it very easy to assign sizes to higher order data structures. They extend natural numbers with a limit…
This paper describes a purely functional library for computing level-$p$-complexity of Boolean functions, and applies it to two-level iterated majority. Boolean functions are simply functions from $n$ bits to one bit, and they can describe…
Toman et al. have proposed a type system for automatic verification of low-level programs, which combines ownership types and refinement types to enable strong updates of refinement types in the presence of pointer aliases. We extend their…
The classical formulation of the program-synthesis problem is to find a program that meets a correctness specification given as a logical formula. Syntax-guided synthesis (SyGuS) is a standardized format for specifying the correctness…
This paper presents a program analysis method that generates program summaries involving polynomial arithmetic. Our approach builds on prior techniques that use solvable polynomial maps for summarizing loops. These techniques are able to…
Optimization pipelines targeting polyhedral programs try to maximize the compute throughput. Traditional approaches favor reuse and temporal locality; while the communicated volume can be low, failure to optimize spatial locality may cause…
The Linux pseudorandom number generator (PRNG) is a PRNG with entropy inputs and is widely used in many security-related applications and protocols. This PRNG is written as an open-source code which is subject to regular changes. It has…
Function merging is a pivotal technique for reducing code size by combining identical or similar functions into a single function. While prior research has extensively explored this technique, it has not been assessed in conjunction with…
Resource leaks occur when a program fails to release a finite resource after it is no longer needed. These leaks are a significant cause of real-world crashes and performance issues. Given their critical impact on software performance and…
High quality epidemiological modelling is essential in order to combat the spread of infectious diseases. In this contribution, we present SimPLoID, an epidemiological modelling framework based on the probabilistic logic programming…
The remarkable growth and significant success of machine learning have expanded its applications into programming languages and program analysis. However, a key challenge in adopting the latest machine learning methods is the representation…
Though LLMs are capable of generating plausible programs, it's challenging to interact with the LLMs further to revise the program, especially if the user's specific requirements are different from the initial proposal. In this paper, we…
Consider the puzzle: given a number, remove $k$ digits such that the resulting number is as large as possible. Various techniques were employed to derive a linear-time solution to the puzzle: predicate logic was used to justify the…
Given a string of parentheses, the task is to find the longest consecutive segment that is balanced, in linear time. We find this problem interesting because it involves a combination of techniques: the usual approach for solving segment…
Reactive languages are dedicated to the programming of systems which interact continuously and concurrently with their environment. Values take the form of unbounded streams modeling the (discrete) passing of time or the sequence of…
Petit is an educational programming language for learning compilers. Students embark on the journey of learning compilers through a series of six tutorials, progressing from topics like lexical analysis and syntactic analysis to semantic…
As the second book in the Anyone Can Code series, Algorithmic Thinking focuses on the logic behind computer programming and software design. With a data-centred approach, it starts with simple algorithms that work on simple data items and…
We present {\lambda}ert, a type theory supporting refinement types with explicit proofs. Instead of solving refinement constraints with an SMT solver like DML and Liquid Haskell, our system requires and permits programmers to embed proofs…