Physical Sciences and Mathematics Commons^™

Proceedings Of The Rust-Edu Workshop, Bart Massey

Rust-Edu Workshop

The 2022 Rust-Edu Workshop was an experiment. We wanted to gather together as many thought leaders we could attract in the area of Rust education, with an emphasis on academic-facing ideas. We hoped that productive discussions and future collaborations would result. Given the quick preparation and the difficulties of an international remote event, I am very happy to report a grand success. We had more than 27 participants from timezones around the globe. We had eight talks, four refereed papers and statements from 15 participants. Everyone seemed to have a good time, and I can say that I learned a …

Functional Programming For Systems Software: Implementing Baremetal Programs In Habit, Donovan Ellison

University Honors Theses

Programming in a baremetal environment, directly on top of hardware with very little to help manage memory or ensure safety, can be dangerous even for experienced programmers. Programming languages can ease the burden on developers and sometimes take care of entire sets of errors. This is not the case for a language like C that will do almost anything you want, for better or worse. To operate in a baremetal environment often requires direct control over memory, but it would be nice to have that capability without sacrificing safety guarantees. Rust is a new language that aims to fit this …

Correct-By-Construction Typechecking With Scope Graphs, Katherine Imhoff Casamento

Dissertations and Theses

Dependently-typed languages are well-known for the ability to enforce program invariants through type signatures, and previous work establishes the effectiveness of this style of program verification in the implementation of type-safe interpreters for a wide class of languages with a variety of interesting scoping semantics, offering an account of dynamic semantics. This thesis covers the complementary topic of static semantics, in the form of a pattern for constructing verified typechecking procedures in a dependently-typed setting. Implementations are given for simply-typed lambda calculus and a small procedural language as well as a module system with unrestricted cyclic module dependency semantics that …

The Nax Language: Unifying Functional Programming And Logical Reasoning In A Language Based On Mendler-Style Recursion Schemes And Term-Indexed Types, Ki Yung Ahn

Dissertations and Theses

Two major applications of lambda calculi in computer science are functional programming languages and mechanized reasoning systems (or, proof assistants). According to the Curry--Howard correspondence, it is possible, in principle, to design a unified language based on a typed lambda calculus for both logical reasoning and programming. However, the different requirements of programming languages and reasoning systems make it difficult to design such a unified language that provides both. Programming languages usually extend lambda calculi with programming-friendly features (e.g., recursive datatypes, general recursion) for supporting the flexibility to model various computations, while sacrificing logical consistency. Logical reasoning systems usually extend …

Interactive Ambient Visualizations For Soft Advice, Emerson Murphy-Hill, Titus Barik, Andrew P. Black

Computer Science Faculty Publications and Presentations

Some software packages offer the user soft advice: recommendations that are intended to help the user create high quality artifacts, but which may turn out to be bad advice. It is left to the user to determine whether the soft advice really will improve quality, and to decide whether or not to adopt it. Visualizations can help the user in making this decision, but we believe that conventional visualizations are less than ideal. In this paper, we describe an interactive ambient visualization to help users identify, understand and interpret soft advice.

Our visualization was developed to help programmers interpret code …

The Grace Programming Language Draft Specification Version 0.3.1261, Andrew P. Black, Kim B. Bruce, James Noble

Computer Science Faculty Publications and Presentations

This is a specification of the Grace Programming Language. This specification is notably incomplete, and everything is subject to change.

Squeak By Example, Andrew P. Black, Stéphane Ducasse, Oscar Nierstrasz, Damien Pollet, Damien Cassou, Marcus Denker

Computer Science Faculty Publications and Presentations

Squeak is a modern open-source development environment for the classic Smalltalk-80 programming language. This book, intended for both students and developers, will guide you gently through the language and tools by means of a series of examples and exercises.

Additional material is available from the book's web page at SqueakByExample.org.

A Framework For Relationship Pattern Languages, Sudarshan Murthy, David Maier

Computer Science Faculty Publications and Presentations

A relationship pattern is an abstraction of a recurring need when establishing relationships among information elements in specific contexts. By developing or leveraging a relationship pattern, modelers can solve a class of problems once and describe many relationship types at once. We have developed a framework for specifying relationship patterns and pattern languages (sets of patterns) in both modeling-language-independent and modeling-language-specific ways. We describe this framework both informally and formally. We provide examples of some commonly observed relationship patterns and show how to use them in ER with the help of a relationship pattern language called Exemplar. We also provide …

Patterns Of Aspect-Oriented Design, Black P. Andrew, James Noble, David J. Pearce, Arno Scmidmeir

Computer Science Faculty Publications and Presentations

Aspect-oriented programming languages are becoming commonplace, and programmers are accumulating experience in building and maintaining aspect-oriented systems. This paper addresses how the use of these languages affects program design: how aspect-oriented languages change the design space, which designs should be emulated and which avoided, and the strengths and weaknesses of particular kinds of design. We identify five patterns of aspect-oriented design: Spectator, Regulator, Patch, Extension, and Heterarchical Design. For each pattern, we describe the problem it solves, show how aspect-oriented language features are used in the pattern, give characteristic examples of the pattern’s use, and assess its benefits and liabilities. …

Directflow: A Domain-Specific Language For Information-Flow Systems, Andrew P. Black, Chuan-Kai Lin

Computer Science Faculty Publications and Presentations

Programs that process streams of information are commonly built by assembling reusable information-flow components. In some systems the components must be chosen from a pre-defined set of primitives; in others the programmer can create new custom components using a general-purpose programming language. Neither approach is ideal: restricting programmers to a set of primitive components limits the expressivity of the system, while allowing programmers to define new components in a general-purpose language makes it difficult or impossible to reason about the composite system. We advocate defining information-flow components in a domain-specific language (DSL) that enables us to infer the properties of …

A Pattern Language For Extensible Program Representation, Andrew P. Black, Daniel Vainsencher

Computer Science Faculty Publications and Presentations

For the last 15 years, implementors of multiple view programming environments have sought a single code model that would form a suitable basis for all of the program analyses and tools that might be applied to the code. They have been unsuccessful. The consequences are a tendency to build monolithic, single-purpose tools, each of which implements its own specialized analyses and optimized representation. This restricts the availability of the analyses, and also limits the reusability of the representation by other tools. Unintegrated tools also produce inconsistent views, which reduce the value of multiple views. This article describes a set of …

Microlanguages For Operating System Specialization, Calton Pu, Andrew P. Black, Crispin Cowan, Jonathan Walpole, Charles Consel

Computer Science Faculty Publications and Presentations

Specialization is a technique that has the potential to provide operating system clients with the performance and functionality that they need, while still retaining the advantages of a simple generic code base for the operating system maintainer. However, at present the specialization process is labor-intensive and requires the knowledge of an expert in the domain of application behavior. In order to realize the full advantages of specialization, we believe that the process must be automated. This means building tools for specialization, and also making the domain knowledge explicit in some form or other. A specialization toolkit has been developed jointly …