-
Logical relations for call-by-push-value models, via internal fibrations in a 2-category
Authors:
Pedro H. Azevedo de Amorim,
Satoshi Kura,
Philip Saville
Abstract:
We give a denotational account of logical relations for call-by-push-value (CBPV) in the fibrational style of Hermida, Jacobs, Katsumata and others. Fibrations -- which axiomatise the usual notion of sets-with-relations -- provide a clean framework for constructing new, logical relations-style, models. Such models can then be used to study properties such as effect simulation.
Extending this pic…
▽ More
We give a denotational account of logical relations for call-by-push-value (CBPV) in the fibrational style of Hermida, Jacobs, Katsumata and others. Fibrations -- which axiomatise the usual notion of sets-with-relations -- provide a clean framework for constructing new, logical relations-style, models. Such models can then be used to study properties such as effect simulation.
Extending this picture to CBPV is challenging: the models incorporate both adjunctions and enrichment, making the appropriate notion of fibration unclear. We handle this using 2-category theory. We identify an appropriate 2-category, and define CBPV fibrations to be fibrations internal to this 2-category which strictly preserve the CBPV semantics.
Next, we develop the theory so it parallels the classical setting. We give versions of the codomain and subobject fibrations, and show that new models can be constructed from old ones by pullback. The resulting framework enables the construction of new, logical relations-style, models for CBPV.
Finally, we demonstrate the utility of our approach with particular examples. These include a generalisation of Katsumata's $\top\top$-lifting to CBPV models, an effect simulation result, and a relative full completeness result for CBPV without sum types.
△ Less
Submitted 20 May, 2025;
originally announced May 2025.
-
Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus (Extended Version)
Authors:
Steven Schaefer,
Nathan Varner,
Pedro H. Azevedo de Amorim,
Max S. New
Abstract:
We present Dependent Lambek Calculus, a domain-specific dependent type theory for verified parsing and formal grammar theory. In $\textrm{Lambek}^D$, linear types are used as a syntax for formal grammars,and parsers can be written as linear terms. The linear typing restriction provides a form of intrinsic verification that a parser yields only valid parse trees for the input string. We demonstrate…
▽ More
We present Dependent Lambek Calculus, a domain-specific dependent type theory for verified parsing and formal grammar theory. In $\textrm{Lambek}^D$, linear types are used as a syntax for formal grammars,and parsers can be written as linear terms. The linear typing restriction provides a form of intrinsic verification that a parser yields only valid parse trees for the input string. We demonstrate the expressivity of this system by showing that the combination of inductive linear types and dependency on non-linear data can be used to encode commonly used grammar formalisms such as regular and context-free grammars as well as traces of various types of automata. Using these encodings, we define parsers for regular expressions using deterministic automata, as well as examples of verified parsers of context-free grammars.
We present a denotational semantics of our type theory that interprets the linear types as functions from strings to sets of abstract parse trees and terms as parse transformers. Based on this denotational semantics, we have made a prototype implementation of $\textrm{Lambek}^D$ using a shallow embedding in the Agda proof assistant. All of our examples parsers have been implemented in this prototype implementation.
△ Less
Submitted 29 April, 2025; v1 submitted 4 April, 2025;
originally announced April 2025.
-
Denotational Foundations for Expected Cost Analysis
Authors:
Pedro H. Azevedo de Amorim
Abstract:
Reasoning about the cost of executing programs is one of the fundamental questions in computer science. In the context of programming with probabilities, however, the notion of cost stops being deterministic, since it depends on the probabilistic samples made throughout the execution of the program. This interaction is further complicated by the non-trivial interaction between cost, recursion and…
▽ More
Reasoning about the cost of executing programs is one of the fundamental questions in computer science. In the context of programming with probabilities, however, the notion of cost stops being deterministic, since it depends on the probabilistic samples made throughout the execution of the program. This interaction is further complicated by the non-trivial interaction between cost, recursion and evaluation strategy.
In this work we introduce $\mathbf{cert}$: a Call-By-Push-Value (CBPV) metalanguage for reasoning about probabilistic cost. We equip $\mathbf{cert}$ with an operational cost semantics and define two denotational semantics -- a cost semantics and an expected-cost semantics. We prove operational soundness and adequacy for the denotational cost semantics and a cost adequacy theorem for the expected-cost semantics.
We formally relate both denotational semantics by stating and proving a novel \emph{effect simulation} property for CBPV. We also prove a canonicity property of the expected-cost semantics as the minimal semantics for expected cost and probability by building on recent advances on monadic probabilistic semantics.
Finally, we illustrate the expressivity of $\mathbf{cert}$ and the expected-cost semantics by presenting case-studies ranging from randomized algorithms to stochastic processes and show how our semantics capture their intended expected cost.
△ Less
Submitted 26 February, 2025; v1 submitted 1 February, 2024;
originally announced February 2024.
-
Modular Hardware Design with Timeline Types
Authors:
Rachit Nigam,
Pedro Henrique Azevedo De Amorim,
Adrian Sampson
Abstract:
Modular design is a key challenge for enabling large-scale reuse of hardware modules. Unlike software, however, hardware designs correspond to physical circuits and inherit constraints from them. Timing constraints -- which cycle a signal arrives, when an input is read -- and structural constraints -- how often a multiplier accepts new inputs -- are fundamental to hardware interfaces. Existing har…
▽ More
Modular design is a key challenge for enabling large-scale reuse of hardware modules. Unlike software, however, hardware designs correspond to physical circuits and inherit constraints from them. Timing constraints -- which cycle a signal arrives, when an input is read -- and structural constraints -- how often a multiplier accepts new inputs -- are fundamental to hardware interfaces. Existing hardware design languages do not provide a way to encode these constraints; a user must read documentation, build scripts, or in the worst case, a module's implementation to understand how to use it. We present Filament, a language for modular hardware design that supports the specification and enforcement of timing and structural constraints for statically scheduled pipelines. Filament uses timeline types, which describe the intervals of clock-cycle time when a given signal is available or required. Filament enables safe composition of hardware modules, ensures that the resulting designs are correctly pipelined, and predictably lowers them to efficient hardware.
△ Less
Submitted 20 April, 2023;
originally announced April 2023.
-
Separated and Shared Effects in Higher-Order Languages
Authors:
Pedro H. Azevedo de Amorim,
Justin Hsu
Abstract:
Effectful programs interact in ways that go beyond simple input-output, making compositional reasoning challenging. Existing work has shown that when such programs are ``separate'', i.e., when programs do not interfere with each other, it can be easier to reason about them. While reasoning about separated resources has been well-studied, there has been little work on reasoning about separated effe…
▽ More
Effectful programs interact in ways that go beyond simple input-output, making compositional reasoning challenging. Existing work has shown that when such programs are ``separate'', i.e., when programs do not interfere with each other, it can be easier to reason about them. While reasoning about separated resources has been well-studied, there has been little work on reasoning about separated effects, especially for functional, higher-order programming languages. We propose two higher-order languages that can reason about sharing and separation in effectful programs. Our first language $λ_{\text{INI}}$ has a linear type system and probabilistic semantics, where the two product types capture independent and possibly-dependent pairs. Our second language $λ_{\text{INI}}^2$ is two-level, stratified language, inspired by Benton's linear-non-linear (LNL) calculus. We motivate this language with a probabilistic model, but we also provide a general categorical semantics and exhibit a range of concrete models beyond probabilistic programming. We prove soundness theorems for all of our languages; our general soundness theorem for our categorical models of $λ_{\text{INI}}^2$ uses a categorical gluing construction.
△ Less
Submitted 2 March, 2023;
originally announced March 2023.
-
Distribution Theoretic Semantics for Non-Smooth Differentiable Programming
Authors:
Pedro H. Azevedo de Amorim,
Christopher Lam
Abstract:
With the wide spread of deep learning and gradient descent inspired optimization algorithms, differentiable programming has gained traction. Nowadays it has found applications in many different areas as well, such as scientific computing, robotics, computer graphics and others. One of its notoriously difficult problems consists in interpreting programs that are not differentiable everywhere.
In…
▽ More
With the wide spread of deep learning and gradient descent inspired optimization algorithms, differentiable programming has gained traction. Nowadays it has found applications in many different areas as well, such as scientific computing, robotics, computer graphics and others. One of its notoriously difficult problems consists in interpreting programs that are not differentiable everywhere.
In this work we define $λ_δ$, a core calculus for non-smooth differentiable programs and define its semantics using concepts from distribution theory, a well-established area of functional analysis. We also show how $λ_δ$ presents better equational properties than other existing semantics and use our semantics to reason about a simplified ray tracing algorithm. Further, we relate our semantics to existing differentiable languages by providing translations to and from other existing differentiable semantic models. Finally, we provide a proof-of-concept implementation in PyTorch of the novel constructions in this paper.
△ Less
Submitted 12 July, 2022;
originally announced July 2022.
-
A Higher-Order Language for Markov Kernels and Linear Operators
Authors:
Pedro H. Azevedo de Amorim
Abstract:
Much work has been done to give semantics to probabilistic programming languages. In recent years, most of the semantics used to reason about probabilistic programs fall in two categories: semantics based on Markov kernels and semantics based on linear operators.
Both styles of semantics have found numerous applications in reasoning about probabilistic programs, but they each have their strength…
▽ More
Much work has been done to give semantics to probabilistic programming languages. In recent years, most of the semantics used to reason about probabilistic programs fall in two categories: semantics based on Markov kernels and semantics based on linear operators.
Both styles of semantics have found numerous applications in reasoning about probabilistic programs, but they each have their strengths and weaknesses. Though it is believed that there is a connection between them there are no languages that can handle both styles of programming.
In this work we address these questions by defining a two-level calculus and its categorical semantics which makes it possible to program with both kinds of semantics. From the logical side of things we see this language as an alternative resource interpretation of linear logic, where the resource being kept track of is sampling instead of variable use.
△ Less
Submitted 2 March, 2023; v1 submitted 31 January, 2022;
originally announced February 2022.
-
First-Order Logic for Flow-Limited Authorization
Authors:
Andrew K. Hirsch,
Pedro H. Azevedo de Amorim,
Ethan Cecchetti,
Ross Tate,
Owen Arden
Abstract:
We present the Flow-Limited Authorization First-Order Logic (FLAFOL), a logic for reasoning about authorization decisions in the presence of information-flow policies. We formalize the FLAFOL proof system, characterize its proof-theoretic properties, and develop its security guarantees. In particular, FLAFOL is the first logic to provide a non-interference guarantee while supporting all connective…
▽ More
We present the Flow-Limited Authorization First-Order Logic (FLAFOL), a logic for reasoning about authorization decisions in the presence of information-flow policies. We formalize the FLAFOL proof system, characterize its proof-theoretic properties, and develop its security guarantees. In particular, FLAFOL is the first logic to provide a non-interference guarantee while supporting all connectives of first-order logic. Furthermore, this guarantee is the first to combine the notions of non-interference from both authorization logic and information-flow systems. All theorems in this paper are proven in Coq.
△ Less
Submitted 28 January, 2020;
originally announced January 2020.
