arXiv subjects

Brigitte Pientka

Publications and source records attributed to Brigitte Pientka.

At least 19 recordsLinked to original sources

arXiv2026

Staged Hybrid Quantum-Classical Programming

Hybrid quantum-classical computing systems consist of a classical control system that sends quantum circuits and receives measurement results from a quantum co-processor. Such systems allow us to model algorithms that require the classical control system to generate quantum circuits on the fly, potentially based on prior measurement results. This is challenging, as the classical control system must generate quantum circuits that manipulate live quantum states. In this setting, the classical control system is generating further quantum circuits while the quantum co-processor is internally maintaining the state of the live qubits; this is not ideal, since this not only is costly but also introduces additional sources of noise to the live qubits. Thus, we want to minimize the latency between receiving measurement results and sending the next quantum circuit to be executed by pre-computing quantum circuits. We introduce HyQ (pronounced haiku), a multi-modal language based on adjoint logic that pre-generates quantum circuits before executing a hybrid quantum-classical program. We achieve this by separating our semantics into two distinct stages: 1) compile-time generation of quantum circuits and classical runtime code and 2) execution of the classical runtime code that instruments the quantum co-processor. This separation between stages allows us to formally guarantee that all circuit-generation logic occurs before the instrumentation logic, i.e., the actual runtime, and minimizes the idling of the quantum co-processor at runtime. We give a type system, a circuit-normalization semantics for the compile-time stage, which eagerly performs all circuit-generation logic, and a runtime semantics for HyQ that corresponds to the second stage. We prove type preservation and progress for both semantics.

cs.PL↗

arXiv2026

Evaluating LLMs in the Context of a Functional Programming Course: A Comprehensive Study

Large-Language Models (LLMs) are changing the way learners acquire knowledge outside the classroom setting. Previous studies have shown that LLMs seem effective in generating to short and simple questions in introductory CS courses using high-resource programming languages such as Java or Python. In this paper, we evaluate the effectiveness of LLMs in the context of a low-resource programming language -- OCaml, in an educational setting. In particular, we built three benchmarks to comprehensively evaluate 9 state-of-the-art LLMs: 1) $\lambda$CodeGen (a benchmark containing natural-language homework programming problems); 2) $\lambda$Repair (a benchmark containing programs with syntax, type, and logical errors drawn from actual student submissions); 3) $\lambda$Explain (a benchmark containing natural language questions regarding theoretical programming concepts). We grade each LLMs responses with respect to correctness using the OCaml compiler and an autograder. And our evaluation goes beyond common evaluation methodology by using manual grading to assess the quality of the responses. Our study shows that the top three LLMs are effective on all tasks within a typical functional programming course, although they solve much fewer homework problems in the low-resource setting compared to their success on introductory programming problems in Python and Java. The strength of LLMs lies in correcting syntax and type errors as well as generating answers to basic conceptual questions. While LLMs may not yet match dedicated language-specific tools in some areas, their convenience as a one-stop tool for multiple programming languages can outweigh the benefits of more specialized systems. We hope our benchmarks can serve multiple purposes: to assess the evolving capabilities of LLMs, to help instructors raise awareness among students about the limitations of LLM-generated solutions, and to inform programming language researchers about opportunities to integrate domain-specific reasoning into LLMs and develop more powerful code synthesis and repair tools for low-resource languages.

cs.PL↗

arXiv2025

Deconstructed Proto-Quipper: A Rational Reconstruction

The Proto-Quipper family of programming languages aims to provide a formal foundation for the Quipper quantum programming language. Unfortunately, Proto-Quipper languages have complex operational semantics: they are inherently effectful, and they rely on set-theoretic operations and fresh name generation to manipulate quantum circuits. This makes them difficult to reason about using standard programming language techniques and, ultimately, to mechanize. We introduce Proto-Quipper-A, a rational reconstruction of Proto-Quipper languages for static circuit generation. It uses a linear $\lambda$-calculus to describe quantum circuits with normal forms that closely correspond to box-and-wire circuit diagrams. Adjoint-logical foundations integrate this circuit language with a linear/non-linear functional language and let us reconstruct Proto-Quipper's circuit programming abstractions using more primitive adjoint-logical operations. Proto-Quipper-A enjoys a simple call-by-value reduction semantics, and to illustrate its tractability as a foundation for Proto-Quipper languages, we show that it is normalizing. We show how to use standard logical relations to prove normalization of linear and substructural systems, thereby avoiding the inherent complexity of existing linear logical relations.

cs.PL↗

arXiv2024

Polymorphic Metaprogramming with Memory Management -- An Adjoint Analysis of Metaprogramming

We describe Elevator, a unifying polymorphic foundation for metaprogramming with memory management based on adjoint modalities. In this setting, we distinguish between multiple memory regions using modes where each mode has a specific set of structural properties. This allows us not only to capture linear (i.e. garbage-free) memory regions and (ordinary) intuitionistic (i.e. garbage-collected or persistent) memory regions, but also to capture accessibility between the memory regions using a preorder between modes. This preorder gives us the power to describe monadic and comonadic programming. As a consequence, it extends the existing logical view of metaprogramming in two directions: first, it ensures that code generation can be done efficiently by controlling memory accesses; second, it allows us to provide resource guarantees about the generated code (i.e. code that is for example garbage-free). We present the static and dynamic semantics of Elevator. In particular, we prove the substructurality of variable references and type safety of the language. We also establish mode safety, which guarantees that the evaluation of a term does not access a value in an inaccessible memory.

cs.PL↗

arXiv2024

Modernizing SMT-Based Type Error Localization

Traditional implementations of strongly-typed functional programming languages often miss the root cause of type errors. As a consequence, type error messages are often misleading and confusing - particularly for students learning such a language. We describe Tyro, a type error localization tool which determines the optimal source of an error for ill-typed programs following fundamental ideas by Pavlinovic et al. : we first translate typing constraints into SMT (Satisfiability Modulo Theories) using an intermediate representation which is more readable than the actual SMT encoding; during this phase we apply a new encoding for polymorphic types. Second, we translate our intermediate representation into an actual SMT encoding and take advantage of recent advancements in off-the-shelf SMT solvers to effectively find optimal error sources for ill-typed programs. Our design maintains the separation of heuristic and search also present in prior and similar work. In addition, our architecture design increases modularity, re-usability, and trust in the overall architecture using an intermediate representation to facilitate the safe generation of the SMT encoding. We believe this design principle will apply to many other tools that leverage SMT solvers. Our experimental evaluation reinforces that the SMT approach finds accurate error sources using both expert-labeled programs and an automated method for larger-scale analysis. Compared to prior work, Tyro lays the basis for large-scale evaluation of error localization techniques, which can be integrated into programming environments and enable us to understand the impact of precise error messages for students in practice.

cs.PL↗

arXiv2024

DeLaM: A Dependent Layered Modal Type Theory for Meta-programming

We scale layered modal type theory to dependent types, introducing DeLaM, dependent layered modal type theory. This type theory is novel in that we have one uniform type theory in which we can not only compose and execute code, but also intensionally analyze the code of types and terms. The latter in particular allows us to write tactics as meta-programs and use regular libraries when writing tactics. DeLaM provides a sound foundation for proof assistants to support type-safe tactic mechanism.

cs.LO↗

arXiv2024

SAT-DIFF: A Tree Diffing Framework Using SAT Solving

Computing differences between tree-structured data is a critical but challenging problem in software analysis. In this paper, we propose a novel tree diffing approach called SatDiff, which reformulates the structural diffing problem into a MaxSAT problem. By encoding the necessary transformations from the source tree to the target tree, SatDiff generates correct, minimal, and type safe low-level edit scripts with formal guarantees. We then synthesize concise high-level edit scripts by effectively merging low-level edits in the appropriate topological order. Our empirical results demonstrate that SatDiff outperforms existing heuristic-based approaches by a significant margin in terms of conciseness while maintaining a reasonable runtime.

cs.PL↗

arXiv2024

Message-Observing Sessions

We present Most, a process language with message-observing session types. Message-observing session types extend binary session types with type-level computation to specify communication protocols that vary based on messages observed on other channels. Hence, Most allows us to express global invariants about processes, rather than just local invariants, in a bottom-up, compositional way. We give Most a semantic foundation using traces with binding, a semantic approach for compositionally reasoning about traces in the presence of name generation. We use this semantics to prove type soundness and compositionality for Most processes. We see this as a significant step towards capturing message-dependencies and providing more precise guarantees about processes.

cs.PL↗

arXiv2024

Adjoint Natural Deduction (Extended Version)

Adjoint logic is a general approach to combining multiple logics with different structural properties, including linear, affine, strict, and (ordinary) intuitionistic logics, where each proposition has an intrinsic mode of truth. It has been defined in the form of a sequent calculus because the central concept of independence is most clearly understood in this form, and because it permits a proof of cut elimination following standard techniques. In this paper we present a natural deduction formulation of adjoint logic and show how it is related to the sequent calculus. As a consequence, every provable proposition has a verification (sometimes called a long normal form). We also give a computational interpretation of adjoint logic in the form of a functional language and prove properties of computations that derive from the structure of modes, including freedom from garbage (for modes without weakening and contraction), strictness (for modes disallowing weakening), and erasure (based on a preorder between modes). Finally, we present a surprisingly subtle algorithm for type checking.

cs.LO↗

arXiv2023

Contextual Refinement Types

We develop an extension of the proof environment Beluga with datasort refinement types and study its impact on mechanized proofs. In particular, we introduce refinement schemas, which provide fine-grained classification for the structures of contexts and binders. Refinement schemas are helpful in concisely representing certain proofs that rely on relations between contexts. Our formulation of refinements combines the type checking and sort checking phases into one by viewing typing derivations as outputs of sorting derivations. This allows us to cleanly state and prove the conservativity of our extension.

cs.PL↗

arXiv2023

Semi-Automation of Meta-Theoretic Proofs in Beluga

We present a sound and complete focusing calculus for the core of the logic behind the proof assistant Beluga as well as an overview of its implementation as a tactic in Beluga's interactive proof environment Harpoon. The focusing calculus is designed to construct uniform proofs over contextual LF and its meta-logic in Beluga: a dependently-typed first-order logic with recursive definitions. The implemented tactic is intended to complete straightforward sub-cases in proofs allowing users to focus only on the interesting aspects of their proofs, leaving tedious simple cases to Beluga's theorem prover. We demonstrate the effectiveness of our work by using the tactic to simplify proving weak-head normalization for the simply-typed lambda-calculus.

cs.PL↗

arXiv2023

Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity

Session types employ a linear type system that ensures that communication channels cannot be implicitly copied or discarded. As a result, many mechanizations of these systems require modeling channel contexts and carefully ensuring that they treat channels linearly. We demonstrate a technique that localizes linearity conditions as additional predicates embedded within type judgments, which allows us to use structural typing contexts instead of linear ones. This technique is especially relevant when leveraging (weak) higher-order abstract syntax to handle channel mobility and the intricate binding structures that arise in session-typed systems. Following this approach, we mechanize a session-typed system based on classical linear logic and its type preservation proof in the proof assistant Beluga, which uses the logical framework LF as its encoding language. We also prove adequacy for our encoding. This shows the tractability and effectiveness of our approach in modelling substructural systems such as session-typed languages.

cs.PL↗

arXiv2023

Layered Modal Type Theories

We introduce layers to modal type theories, which subsequently enables type theories for pattern matching on code in meta-programming and clean and straightforward semantics.

cs.LO↗

arXiv2023

Can ChatGPT Pass An Introductory Level Functional Language Programming Course?

The recent introduction of ChatGPT has drawn significant attention from both industry and academia due to its impressive capabilities in solving a diverse range of tasks, including language translation, text summarization, and computer programming. Its capability for writing, modifying, and even correcting code together with its ease of use and access is already dramatically impacting computer science education. This paper aims to explore how well ChatGPT can perform in an introductory-level functional language programming course. In our systematic evaluation, we treated ChatGPT as one of our students and demonstrated that it can achieve a grade B- and its rank in the class is 155 out of 314 students overall. Our comprehensive evaluation provides valuable insights into ChatGPT's impact from both student and instructor perspectives. Additionally, we identify several potential benefits that ChatGPT can offer to both groups. Overall, we believe that this study significantly clarifies and advances our understanding of ChatGPT's capabilities and potential impact on computer science education.

cs.CY↗

arXiv2023

Identifying Different Student Clusters in Functional Programming Assignments: From Quick Learners to Struggling Students

Instructors and students alike are often focused on the grade in programming assignments as a key measure of how well a student is mastering the material and whether a student is struggling. This can be, however, misleading. Especially when students have access to auto-graders, their grades may be heavily skewed. In this paper, we analyze student assignment submission data collected from a functional programming course taught at McGill university incorporating a wide range of features. In addition to the grade, we consider activity time data, time spent, and the number of static errors. This allows us to identify four clusters of students: "Quick-learning", "Hardworking", "Satisficing", and "Struggling" through cluster algorithms. We then analyze how work habits, working duration, the range of errors, and the ability to fix errors impact different clusters of students. This structured analysis provides valuable insights for instructors to actively help different types of students and emphasize different aspects of their overall course design. It also provides insights for students themselves to understand which aspects they still struggle with and allows them to seek clarification and adjust their work habits.

cs.CY↗

arXiv2022

A Categorical Normalization Proof for the Modal Lambda-Calculus

We investigate a simply typed modal $\lambda$-calculus, $\lambda^{\to\square}$, due to Pfenning, Wong and Davies, where we define a well-typed term with respect to a context stack that captures the possible world semantics in a syntactic way. It provides logical foundation for multi-staged meta-programming. Our main contribution in this paper is a normalization by evaluation (NbE) algorithm for $\lambda^{\to\square}$ which we prove sound and complete. The NbE algorithm is a moderate extension to the standard presheaf model of simply typed $\lambda$-calculus. However, central to the model construction and the NbE algorithm is the observation of Kripke-style substitutions on context stacks which brings together two previously separate concepts, structural modal transformations on context stacks and substitutions for individual assumptions. Moreover, Kripke-style substitutions allow us to give a formulation for contextual types, which can represent open code in a meta-programming setting. Our work lays the foundation for extending the logical foundation by Pfenning, Wong, and Davies towards building a practical, dependently typed foundation for meta-programming.

cs.PL↗

arXiv2022

Novice Type Error Diagnosis with Natural Language Models

Strong static type systems help programmers eliminate many errors without much burden of supplying type annotations. However, this flexibility makes it highly non-trivial to diagnose ill-typed programs, especially for novice programmers. Compared to classic constraint solving and optimization-based approaches, the data-driven approach has shown great promise in identifying the root causes of type errors with higher accuracy. Instead of relying on hand-engineered features, this work explores natural language models for type error localization, which can be trained in an end-to-end fashion without requiring any features. We demonstrate that, for novice type error diagnosis, the language model-based approach significantly outperforms the previous state-of-the-art data-driven approach. Specifically, our model could predict type errors correctly 62% of the time, outperforming the state-of-the-art Nate's data-driven model by 11%, in a more rigorous accuracy metric. Furthermore, we also apply structural probes to explain the performance difference between different language models.

cs.PL↗

arXiv2022

An Investigation of Kripke-style Modal Type Theories

This technical report investigates Kripke-style modal type theories, both simply typed and dependently typed. We examine basic meta-theories of the type theories, develop their substitution calculi, and give normalization by evaluation algorithms.

cs.LO↗