26,098 papers · page 208 of 1,305
Matthew Dinmore
During the 1990s and first decade of the 2000s, problem-solving environments (PSEs) were a topic of research among a community with the vision to create software systems “with all of the computational facilities necessary to solve a target class of problems.” Use of the term has …
Beniamino Accattoli
The λ-calculus models the core of functional programming languages. This essay discusses a gap between the theory of the λ-calculus and functional languages, namely the fact that the former does not give a status to sharing, the essential ingredient for efficiency in the lattter.…
James Noble, Robert Biddle
Programming languages are languages --- “unnatural” languages because they are constructed explicitly; “formal” languages because they rely on mathematical notations and are described mathematically; “machine” languages because they are used to communicate with machines. Above al…
Sean Hadar, Shachar Itzhaky
Spreadsheets are a popular programming model among both novice and advanced users. It allows for quick development of computational tasks over the user's data set. It has also been suggested as a model for lightweight, low-code development of small-scale personal and collaborativ…
Mathijs Schuts, Jozef Hooman
We present our vision for creating an industrial legacy software rejuvenation toolchain. The goal is to semi automatically remove code smells from stateful software used in Cyber Physical Systems (CPS). Compared to existing tools that remove code smells, our toolchain can remove …
Samyak Jhaveri, Alberto Krone-Martins, Cristina V. Lopes
Quantum computers are becoming a reality. The advantage of quantum computing is that it has the potential to solve computationally complex problems in a fixed amount time, independent of the size of the problem. However, the kinds of problems for which these computers are a good …
Colin S. Gordon, Sergey Matskevich
Interactive proof assistants are computer programs carefully constructed to check a human-designed proof of a mathematical claim with high confidence in the implementation. However, this only validates truth of a formal claim, which may have been mistranslated from a claim made i…
André Teles, André Santos
Conventionally, merging code files is performed using generic line-based merging algorithms (e.g., diff3) that are unaware of the syntax and semantics of the programming language, outputting conflicts that could be avoided. Structured and semistructured merging techniques are cap…
Christoph Thiede, Marcel Taeumel, Robert Hirschfeld
Exploration of state and behavior is essential for understanding and debugging object-oriented programs. Many time-related questions about object communication – an object’s history – only arise in the context of a specific error in the here and now. At such a specific point in t…
Assaf Avishahar-Zeira, David H. Lorenz
By 2030 for each filled position in Software Engineering, two positions would remain unfilled. This already apparent loss of productivity has the software industry scrambling to fill the missing positions with citizen developers---technical people with little or no programming sk…
Peter Wilczynski, Taylor Gregoire-Wright, Daniel Jackson
Developers have long recognized the importance of the concepts underlying the systems they build, and the primary role that concepts play in shaping user experience. To date, however, concepts have tended to be only implicit in software design with development being organized ins…
Mark Marron
Integration, composition, mechanization, and AI assisted development are the driving themes in the future of software development. At their core these concepts are rooted in the increasingly important role of computing in our world, the desire to deliver functionality faster, wit…
Siddharth Bhaskar, Jakob Grue Simonsen
Abstract In the cons-free programming paradigm, we eschew constructors and program using only destructors. Cons-free programs in a simple first-order language with string data capture exactly P, the class of polynomial-time relations. By varying the underlying language and consid…
Jonathan Chan, Yufeng Li, William J. Bowman
Abstract Contemporary proof assistants such as Coq require that recursive functions be terminating and corecursive functions be productive to maintain logical consistency of their type theories, and some ensure these properties using syntactic checks. However, being syntactic, th…
Olivier Danvy
Abstract The equivalence of folding left and right over Peano numbers and lists makes it possible to minimalistically inter-derive (1) structurally recursive functions in direct style, (2) structurally tail-recursive functions that use an accumulator, and (3) structurally tail-re…
Olivier Danvy
Paul Downen, Zena M. Ariola
Abstract Recursion is a mature, well-understood topic in the theory and practice of programming. Yet its dual, corecursion is underappreciated and still seen as exotic. We aim to put them both on equal footing by giving a foundation for primitive corecursion based on computation,…
Ralf Hinze
The other day, I was assembling lecture material for a course on Agda. Pursuing an application-driven approach, I was looking for correctness proofs of popular algorithms. One of my all-time favourites is Huffman data compression (Huffman, 1952). Even though it is probably safe t…
Jason Z. S. Hu, Junyoung Jang, Brigitte Pientka
Abstract We present the Kripke-style modal type theory, Mint , which combines dependent types and the necessity modality. It extends the Kripke-style modal lambda-calculus by Pfenning and Davies to the full Martin-Löf type theory. As such it encompasses dependently typed variants…
Graham Hutton
Abstract Programming language semantics is an important topic in theoretical computer science, but one that beginners often find challenging. This article provides a tutorial introduction to the subject, in which the language of integers and addition is used as a minimal setting …