arXiv subjects

Andrew D. Gordon

Publications and source records attributed to Andrew D. Gordon.

18 recordsLinked to original sources

arXiv2026

The LLMbda Calculus: AI Agents, Conversations, and Information Flow

Large language models are increasingly deployed as agents: they plan, call tools, read untrusted data, and act on the results. This exposes them to prompt injection: data meant only to be read is obeyed as an instruction. The most principled defences replace content inspection with provenance: classifying data by source and keeping trusted and untrusted apart through a separation of duty (the dual-LLM pattern) and information-flow control. Yet the leading systems are hard to fully trust: flow tracking is easy to get wrong, deliberate relaxations are hard to audit, and the dual-LLM pattern is hard-wired into the architecture. We present LLMbda, an untyped call-by-value lambda calculus that makes provenance-based defence both expressible and provably sound, without committing to an architecture. It adds the operational core of agentic systems as first-class constructs: prompt-response conversations that can be forked and cleared, code generation, and dynamic information-flow control in which every value carries a label that every reduction propagates. Isolation becomes a policy a program expresses, and reclassification an explicit, auditable construct. Our central result is a termination-insensitive probabilistic noninterference theorem over the whole calculus, including code-generating agents, with an insulated variant that holds even when the attacker chooses all untrusted inputs. The verified interpreter is itself the harness that calls the model, to our knowledge the first LLM agent harness whose executable is the subject of machine-checked security theorems, so every agent inherits the guarantee. On the AgentDojo banking benchmark, an agent built within LLMbda, enforcement always on, matches the utility of CaMeL, a leading dual-LLM defence, run without its policy checks (which halve its utility), and resists all but two of 1296 attacked runs. Our harness and all proofs are in Lean.

cs.PL↗

arXiv2024

Requirements are All You Need: The Final Frontier for End-User Software Engineering

What if end users could own the software development lifecycle from conception to deployment using only requirements expressed in language, images, video or audio? We explore this idea, building on the capabilities that generative Artificial Intelligence brings to software generation and maintenance techniques. How could designing software in this way better serve end users? What are the implications of this process for the future of end-user software engineering and the software development lifecycle? We discuss the research needed to bridge the gap between where we are today and these imagined systems of the future.

cs.SE↗

arXiv2024

"My toxic trait is thinking I'll remember this": gaps in the learner experience of video tutorials for feature-rich software

Video tutorials are a popular medium for informal and formal learning. However, when learners attempt to view and follow along with these tutorials, they encounter what we call gaps, that is, issues that can prevent learning. We examine the gaps encountered by users of video tutorials for feature-rich software, such as spreadsheets. We develop a theory and taxonomy of such gaps, identifying how they act as barriers to learning, by collecting and analyzing 360 viewer comments from 90 Microsoft Excel video tutorials published by 43 creators across YouTube, TikTok, and Instagram. We conducted contextual interviews with 8 highly influential tutorial creators to investigate the gaps their viewers experience and how they address them. Further, we obtain insights into their creative process and frustrations when creating video tutorials. Finally, we present creators with two designs that aim to address gaps identified in the comment analysis for feedback and alternative design ideas.

cs.HC↗

arXiv2024

Solving Data-centric Tasks using Large Language Models

Large language models (LLMs) are rapidly replacing help forums like StackOverflow, and are especially helpful for non-professional programmers and end users. These users are often interested in data-centric tasks, such as spreadsheet manipulation and data wrangling, which are hard to solve if the intent is only communicated using a natural-language description, without including the data. But how do we decide how much data and which data to include in the prompt? This paper makes two contributions towards answering this question. First, we create a dataset of real-world NL-to-code tasks manipulating tabular data, mined from StackOverflow posts. Second, we introduce a cluster-then-select prompting technique, which adds the most representative rows from the input data to the LLM prompt. Our experiments show that LLM performance is indeed sensitive to the amount of data passed in the prompt, and that for tasks with a lot of syntactic variation in the input table, our cluster-then-select technique outperforms a random selection baseline.

cs.PL↗

arXiv2023

Participatory prompting: a user-centric research method for eliciting AI assistance opportunities in knowledge workflows

Generative AI, such as image generation models and large language models, stands to provide tremendous value to end-user programmers in creative and knowledge workflows. Current research methods struggle to engage end-users in a realistic conversation that balances the actually existing capabilities of generative AI with the open-ended nature of user workflows and the many opportunities for the application of this technology. In this work-in-progress paper, we introduce participatory prompting, a method for eliciting opportunities for generative AI in end-user workflows. The participatory prompting method combines a contextual inquiry and a researcher-mediated interaction with a generative model, which helps study participants interact with a generative model without having to develop prompting strategies of their own. We discuss the ongoing development of a study whose aim will be to identify end-user programming opportunities for generative AI in data analysis workflows.

cs.HC↗

arXiv2023

Co-audit: tools to help humans double-check AI-generated content

Users are increasingly being warned to check AI-generated content for correctness. Still, as LLMs (and other generative models) generate more complex output, such as summaries, tables, or code, it becomes harder for the user to audit or evaluate the output for quality or correctness. Hence, we are seeing the emergence of tool-assisted experiences to help the user double-check a piece of AI-generated content. We refer to these as co-audit tools. Co-audit tools complement prompt engineering techniques: one helps the user construct the input prompt, while the other helps them check the output response. As a specific example, this paper describes recent research on co-audit tools for spreadsheet computations powered by generative models. We explain why co-audit experiences are essential for any application of generative AI where quality is important and errors are consequential (as is common in spreadsheet computations). We propose a preliminary list of principles for co-audit, and outline research challenges.

cs.HC↗

arXiv2023

"What It Wants Me To Say": Bridging the Abstraction Gap Between End-User Programmers and Code-Generating Large Language Models

Code-generating large language models translate natural language into code. However, only a small portion of the infinite space of naturalistic utterances is effective at guiding code generation. For non-expert end-user programmers, learning this is the challenge of abstraction matching. We examine this challenge in the specific context of data analysis in spreadsheets, in a system that maps the users natural language query to Python code using the Codex generator, executes the code, and shows the result. We propose grounded abstraction matching, which bridges the abstraction gap by translating the code back into a systematic and predictable naturalistic utterance. In a between-subjects, think-aloud study (n=24), we compare grounded abstraction matching to an ungrounded alternative based on previously established query framing principles. We find that the grounded approach improves end-users' understanding of the scope and capabilities of the code-generating model, and the kind of language needed to use it effectively.

cs.HC↗

arXiv2022

What is it like to program with artificial intelligence?

Large language models, such as OpenAI's codex and Deepmind's AlphaCode, can generate code to solve a variety of problems expressed in natural language. This technology has already been commercialised in at least one widely-used programming editor extension: GitHub Copilot. In this paper, we explore how programming with large language models (LLM-assisted programming) is similar to, and differs from, prior conceptualisations of programmer assistance. We draw upon publicly available experience reports of LLM-assisted programming, as well as prior usability and design studies. We find that while LLM-assisted programming shares some properties of compilation, pair programming, and programming via search and reuse, there are fundamental differences both in the technical possibilities as well as the practical experience. Thus, LLM-assisted programming ought to be viewed as a new way of programming with its own distinct properties and challenges. Finally, we draw upon observations from a user study in which non-expert end user programmers use LLM-assisted tools for solving data tasks in spreadsheets. We discuss the issues that might arise, and open research challenges, in applying large language models to end-user programming, particularly with users who have little or no programming expertise.

cs.HC↗

arXiv2022

Conditional independence by typing

A central goal of probabilistic programming languages (PPLs) is to separate modelling from inference. However, this goal is hard to achieve in practice. Users are often forced to re-write their models in order to improve efficiency of inference or meet restrictions imposed by the PPL. Conditional independence (CI) relationships among parameters are a crucial aspect of probabilistic models that capture a qualitative summary of the specified model and can facilitate more efficient inference. We present an information flow type system for probabilistic programming that captures conditional independence (CI) relationships, and show that, for a well-typed program in our system, the distribution it implements is guaranteed to have certain CI-relationships. Further, by using type inference, we can statically deduce which CI-properties are present in a specified model. As a practical application, we consider the problem of how to perform inference on models with mixed discrete and continuous parameters. Inference on such models is challenging in many existing PPLs, but can be improved through a workaround, where the discrete parameters are used implicitly, at the expense of manual model re-writing. We present a source-to-source semantics-preserving transformation, which uses our CI-type system to automate this workaround by eliminating the discrete parameters from a probabilistic program. The resulting program can be seen as a hybrid inference algorithm on the original program, where continuous parameters can be drawn using efficient gradient-based inference methods, while the discrete parameters are inferred using variable elimination. We implement our CI-type system and its example application in SlicStan: a compositional variant of Stan.

cs.PL↗

arXiv2021

OptTyper: Probabilistic Type Inference by Optimising Logical and Natural Constraints

We present a new approach to the type inference problem for dynamic languages. Our goal is to combine \emph{logical} constraints, that is, deterministic information from a type system, with \emph{natural} constraints, that is, uncertain statistical information about types learnt from sources like identifier names. To this end, we introduce a framework for probabilistic type inference that combines logic and learning: logical constraints on the types are extracted from the program, and deep learning is applied to predict types from surface-level code properties that are statistically associated. The foremost insight of our method is to constrain the predictions from the learning procedure to respect the logical constraints, which we achieve by relaxing the logical inference problem of type prediction into a continuous optimisation problem. We build a tool called OptTyper to predict missing types for TypeScript files. OptTyper combines a continuous interpretation of logical constraints derived by classical static analysis of TypeScript code, with natural constraints obtained from a deep learning model, which learns naming conventions for types from a large codebase. By evaluating OptTyper, we show that the combination of logical and natural constraints yields a large improvement in performance over either kind of information individually and achieves a 4% improvement over the state-of-the-art.

cs.PL↗

arXiv2019

Somewhere Around That Number: An Interview Study of How Spreadsheet Users Manage Uncertainty

Spreadsheet users regularly deal with uncertainty in their data, for example due to errors and estimates. While an insight into data uncertainty can help in making better informed decisions, prior research suggests that people often use informal heuristics to reason with probabilities, which leads to incorrect conclusions. Moreover, people often ignore or simplify uncertainty. To understand how people currently encounter and deal with uncertainty in spreadsheets, we conducted an interview study with 11 spreadsheet users from a range of domains. We found that how people deal with uncertainty is influenced by the role the spreadsheet plays in people's work and the user's aims. Spreadsheets are used as a database, template, calculation tool, notepad and exploration tool. In doing so, participants' aims were to compute and compare different scenarios, understand something about the nature of the uncertainty in their situation, and translate the complexity of data uncertainty into simplified presentations to other people, usually decision-makers. Spreadsheets currently provide limited tools to support these aims, and participants had various workarounds.

cs.HC↗

arXiv2018

Probabilistic Programming with Densities in SlicStan: Efficient, Flexible and Deterministic

Stan is a probabilistic programming language that has been increasingly used for real-world scalable projects. However, to make practical inference possible, the language sacrifices some of its usability by adopting a block syntax, which lacks compositionality and flexible user-defined functions. Moreover, the semantics of the language has been mainly given in terms of intuition about implementation, and has not been formalised. This paper provides a formal treatment of the Stan language, and introduces the probabilistic programming language SlicStan --- a compositional, self-optimising version of Stan. Our main contributions are: (1) the formalisation of a core subset of Stan through an operational density-based semantics; (2) the design and semantics of the Stan-like language SlicStan, which facilities better code reuse and abstraction through its compositional syntax, more flexible functions, and information-flow type system; and (3) a formal, semantic-preserving procedure for translating SlicStan to Stan.

cs.PL↗

arXiv2017

Deriving Probability Density Functions from Probabilistic Functional Programs

The probability density function of a probability distribution is a fundamental concept in probability theory and a key ingredient in various widely used machine learning methods. However, the necessary framework for compiling probabilistic functional programs to density functions has only recently been developed. In this work, we present a density compiler for a probabilistic language with failure and both discrete and continuous distributions, and provide a proof of its soundness. The compiler greatly reduces the development effort of domain experts, which we demonstrate by solving inference problems from various scientific applications, such as modelling the global carbon cycle, using a standard Markov chain Monte Carlo framework.

cs.PL↗

arXiv2017

A Lambda-Calculus Foundation for Universal Probabilistic Programming

We develop the operational semantics of an untyped probabilistic lambda-calculus with continuous distributions, as a foundation for universal probabilistic programming languages such as Church, Anglican, and Venture. Our first contribution is to adapt the classic operational semantics of lambda-calculus to a continuous setting via creating a measure space on terms and defining step-indexed approximations. We prove equivalence of big-step and small-step formulations of this distribution-based semantics. To move closer to inference techniques, we also define the sampling-based semantics of a term as a function from a trace of random samples to a value. We show that the distribution induced by integrating over all traces equals the distribution-based semantics. Our second contribution is to formalize the implementation technique of trace Markov chain Monte Carlo (MCMC) for our calculus and to show its correctness. A key step is defining sufficient conditions for the distribution induced by trace MCMC to converge to the distribution-based semantics. To the best of our knowledge, this is the first rigorous correctness proof for trace MCMC for a higher-order functional language.

cs.PL↗

arXiv2013

Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols

We describe how to verify security properties of C code for cryptographic protocols by using a general-purpose verifier. We prove security theorems in the symbolic model of cryptography. Our techniques include: use of ghost state to attach formal algebraic terms to concrete byte arrays and to detect collisions when two distinct terms map to the same byte array; decoration of a crypto API with contracts based on symbolic terms; and expression of the attacker model in terms of C programs. We rely on the general-purpose verifier VCC; we guide VCC to prove security simply by writing suitable header files and annotations in implementation files, rather than by changing VCC itself. We formalize the symbolic model in Coq in order to justify the addition of axioms to VCC.

cs.CR↗

arXiv2011

Extracting and Verifying Cryptographic Models from C Protocol Code by Symbolic Execution

Consider the problem of verifying security properties of a cryptographic protocol coded in C. We propose an automatic solution that needs neither a pre-existing protocol description nor manual annotation of source code. First, symbolically execute the C program to obtain symbolic descriptions for the network messages sent by the protocol. Second, apply algebraic rewriting to obtain a process calculus description. Third, run an existing protocol analyser (ProVerif) to prove security properties or find attacks. We formalise our algorithm and appeal to existing results for ProVerif to establish computational soundness under suitable circumstances. We analyse only a single execution path, so our results are limited to protocols with no significant branching. The results in this paper provide the first computationally sound verification of weak secrecy and authentication for (single execution paths of) C code.

cs.CR↗

arXiv2004

TulaFale: A Security Tool for Web Services

Web services security specifications are typically expressed as a mixture of XML schemas, example messages, and narrative explanations. We propose a new specification language for writing complementary machine-checkable descriptions of SOAP-based security protocols and their properties. Our TulaFale language is based on the pi calculus (for writing collections of SOAP processors running in parallel), plus XML syntax (to express SOAP messaging), logical predicates (to construct and filter SOAP messages), and correspondence assertions (to specify authentication goals of protocols). Our implementation compiles TulaFale into the applied pi calculus, and then runs Blanchet's resolution-based protocol verifier. Hence, we can automatically verify authentication properties of SOAP protocols.

cs.CR↗

arXiv2004

Validating a Web Service Security Abstraction by Typing

An XML web service is, to a first approximation, an RPC service in which requests and responses are encoded in XML as SOAP envelopes, and transported over HTTP. We consider the problem of authenticating requests and responses at the SOAP-level, rather than relying on transport-level security. We propose a security abstraction, inspired by earlier work on secure RPC, in which the methods exported by a web service are annotated with one of three security levels: none, authenticated, or both authenticated and encrypted. We model our abstraction as an object calculus with primitives for defining and calling web services. We describe the semantics of our object calculus by translating to a lower-level language with primitives for message passing and cryptography. To validate our semantics, we embed correspondence assertions that specify the correct authentication of requests and responses. By appeal to the type theory for cryptographic protocols of Gordon and Jeffrey's Cryptyc, we verify the correspondence assertions simply by typing. Finally, we describe an implementation of our semantics via custom SOAP headers.

cs.CR↗