54 citations · 90 across the 12 of their papers we have counts for
12 papers
Symmetries in Sorting
Vikraman Choudhury, Wind Wong
Sorting algorithms are fundamental to computer science, and their correctness criteria are well understood as rearranging elements of a list according to a specified total order on…
Intrinsically Correct Sorting in Cubical Agda
Cass Alexandru, Vikraman Choudhury, Jurriaan Rot +1
The paper "Sorting with Bialgebras and Distributive Laws" by Hinze et al. uses the framework of bialgebraic semantics to define sorting algorithms. From distributive laws between f…
Towards Quantum Multiparty Session Types
Ivan Lanese, Ugo Dal Lago, Vikraman Choudhury
Multiparty Session Types (MPSTs) offer a structured way of specifying communication protocols and guarantee relevant communication properties, such as deadlock-freedom. In this pap…
Scheme Pearl: Quantum Continuations
Vikraman Choudhury, Borislav Agapiev, Amr Sabry
We advance the thesis that the simulation of quantum circuits is fundamentally about the efficient management of a large (potentially exponential) number of delimited continuations…
Symmetries in Reversible Programming: From Symmetric Rig Groupoids to Reversible Programming Languages
Vikraman Choudhury, Jacek Karwowski, Amr Sabry
The family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic datatypes. In this…
Free Commutative Monoids in Homotopy Type Theory
Vikraman Choudhury, Marcelo Fiore
We develop a constructive theory of finite multisets in Homotopy Type Theory, defining them as free commutative monoids. After recalling basic structural properties of the free com…
Fractional Types: Expressive and Safe Space Management for Ancilla Bits
Chao-Hong Chen, Vikraman Choudhury, Jacques Carette +1
In reversible computing, the management of space is subject to two broad classes of constraints. First, as with general-purpose computation, every allocation must be paired with a…
Recovering Purity with Comonads and Capabilities
Vikraman Choudhury, Neel Krishnaswami
In this paper, we take a pervasively effectful (in the style of ML) typed lambda calculus, and show how to extend it to permit capturing pure expressions with types. Our key observ…
Refinement Reflection: Complete Verification with SMT
Niki Vazou, Anish Tondwalkar, Vikraman Choudhury +4
We introduce Refinement Reflection, a new framework for building SMT-based deductive verifiers. The key idea is to reflect the code implementing a user-defined function into the fu…
From Reversible Programs to Univalent Universes and Back
Jacques Carette, Chao-Hong Chen, Vikraman Choudhury +1
We establish a close connection between a reversible programming language based on type isomorphisms and a formally presented univalent universe. The correspondence relates combina…
Deriving Law-Abiding Instances
Ryan Scott, Vikraman Choudhury, Ryan Newton +2
Liquid Haskell's refinement-reflection feature augments the Haskell language with theorem proving capabilities, allowing programmers to retrofit their existing code with proofs. Bu…
Adaptive Lock-Free Data Structures in Haskell: A General Method for Concurrent Implementation Swapping
Chao-Hong Chen, Vikraman Choudhury, Ryan R. Newton
A key part of implementing high-level languages is providing built-in and default data structures. Yet selecting good defaults is hard. A mutable data structure's workload is not k…