Wed 18 Jan 2023 18:00 - 19:30 at Grand Ballroom A - SRC Poster Chair(s): Jeehoon Kang, Danfeng Zhang

Superconductor electronics (SCE) is an emerging hardware technology that allows for highly power-efficient circuit designs. SCE circuits are based on inherently stateful gates that communicate via transient \textit{pulses}, in contrast to conventional CMOS technology that uses stateless gates that communicate via low vs high voltage levels (the traditional ‘zeroes’ and ‘ones’ of Boolean logic). These differences mean that decades of optimizations and techniques for reasoning about hardware designs are rendered obsolete for SCE designs. Advancing the state of SCE requires new techniques for formally reasoning about SCE designs and notions of equivalence and other relations between SCE circuits.

In this paper we describe Citrus, an embedded DSL in the dependently-typed language Agda for describing SCE circuits that allows for equational reasoning about SCE circuit equivalence. Citrus provides a formal description of SCE gates by embedding them into the theory of arrows and provides tools to reason about equivalence between circuits in the form of time-abstract bisimulation. We evaluate Citrus using a case study in which we prove that an SCE circuit optimization, previously proposed by people working on real SCE circuits but heretofore unproven to be correct, is indeed a semantics-preserving transformation.

Wed 18 Jan

Displayed time zone: Eastern Time (US & Canada) change

18:00 - 19:30
SRC PosterStudent Research Competition at Grand Ballroom A
Chair(s): Jeehoon Kang KAIST, Danfeng Zhang Pennsylvania State University
18:00
90m
Talk
Zydeco: A Stack-Based Call-By-Push-Value Language
Student Research Competition
Yuchen Jiang University of Michigan, Runze Xue CSE Department at the University of Michigan
18:00
90m
Talk
HasChor: Choreographic Programming in Haskell
Student Research Competition
Gan Shen University of California, Santa Cruz, USA
18:00
90m
Talk
Towards Synthesis in Superposition
Student Research Competition
18:00
90m
Talk
A Formalization of Observational Equivalence in Message Passing Protocols
Student Research Competition
Nathan Liittschwager University of California, Santa Cruz
18:00
90m
Talk
On the metatheory of IRs and the CPS-calculus
Student Research Competition
Paulo Torrens University of Kent
18:00
90m
Talk
Scalable Synthesis of Regular Expressions From Only Positive Examples
Student Research Competition
18:00
90m
Talk
Evaluating Soundness of a Gradual Verifier with Property Based Testing
Student Research Competition
Jan-Paul Ramos-Davila Cornell University
18:00
90m
Talk
A mechanized model for logical clocks
Student Research Competition
Jonathan Castello UC Santa Cruz
18:00
90m
Talk
Wisening Assertions: A live Bayesian reasoning system for probabilistic correctness
Student Research Competition
Joshua Turcotti Cornell University
18:00
90m
Talk
Synthesizing Vectorized Code via Verified Lifting
Student Research Competition
Jeremy Ferguson University of California-Berkeley
18:00
90m
Talk
Citrus: A Dependently Typed Framework for Pulse-Based Logic
Student Research Competition
Harlan Kringen UC Santa Barbara, Ben Hardekopf University of California at Santa Barbara
18:00
90m
Talk
Neko: A quantum map-filter-reduce programming language
Student Research Competition
Elton Pinto Georgia Institute of Technology
18:00
90m
Talk
Compiling and Running High-level Quantum Programs
Student Research Competition
18:00
90m
Talk
Trace-Guided Inductive Synthesis of Recursive Functional Programs
Student Research Competition
Yongwei Yuan Purdue University