-
Sharing Neurophysiology Data from the Allen Brain Observatory: Lessons Learned
Authors:
Saskia E. J. de Vries,
Joshua H. Siegle,
Christof Koch
Abstract:
Making all data for any observation or experiment openly available is a defining feature of empirical science (e.g., nullius in verba, the motto of the Royal Society). It enhances transparency, reproducibility, and societal trust. While embraced in spirit by many, in practice open data sharing remains the exception in contemporary systems neuroscience. Here, we take stock of the Allen Brain Observ…
▽ More
Making all data for any observation or experiment openly available is a defining feature of empirical science (e.g., nullius in verba, the motto of the Royal Society). It enhances transparency, reproducibility, and societal trust. While embraced in spirit by many, in practice open data sharing remains the exception in contemporary systems neuroscience. Here, we take stock of the Allen Brain Observatory, an effort to share data and metadata associated with surveys of neuronal activity in the visual system of laboratory mice. The data from these surveys have been used to produce new discoveries, to validate computational algorithms, and as a benchmark for comparison with other data, resulting in over 100 publications and preprints to date. We distill some of the lessons learned about open surveys and data reuse, including remaining barriers to data sharing and what might be done to address these.
△ Less
Submitted 16 December, 2022;
originally announced December 2022.
-
Searching Entangled Program Spaces
Authors:
James Koppel,
Zheng Guo,
Edsko de Vries,
Armando Solar-Lezama,
Nadia Polikarpova
Abstract:
Many problem domains, including program synthesis and rewrite-based optimization, require searching astronomically large spaces of programs. Existing approaches often rely on building specialized data structures -- version-space algebras, finite tree automata, or e-graphs -- to compactly represent these programs. To find a compact representation, existing data structures exploit independence of su…
▽ More
Many problem domains, including program synthesis and rewrite-based optimization, require searching astronomically large spaces of programs. Existing approaches often rely on building specialized data structures -- version-space algebras, finite tree automata, or e-graphs -- to compactly represent these programs. To find a compact representation, existing data structures exploit independence of subterms; they blow up when the choices of subterms are entangled. We introduce equality-constrained tree automata (ECTAs), a generalization of the three aforementioned data structures that can efficiently represent large spaces of programs with entangled subterms. We present efficient algorithms for extracting programs from ECTAs, implemented in a performant Haskell library, \texttt{ecta}. Using \texttt{ecta} we construct \textsc{Hectare}, a type-driven program synthesizer for Haskell. \textsc{Hectare} significantly outperforms a state-of-the-art synthesizer Hoogle+ -- providing an average speedup of 8x -- despite its implementation being an order of magnitude smaller.
△ Less
Submitted 15 June, 2022;
originally announced June 2022.
-
Locally Nameless Permutation Types
Authors:
Edsko de Vries,
Vasileios Koutavas
Abstract:
We define "Locally Nameless Permutation Types", which fuse permutation types as used in Nominal Isabelle with the locally nameless representation. We show that this combination is particularly useful when formalizing programming languages where bound names may become free during execution ("extrusion"), common in process calculi. It inherits the generic definition of permutations and support, and…
▽ More
We define "Locally Nameless Permutation Types", which fuse permutation types as used in Nominal Isabelle with the locally nameless representation. We show that this combination is particularly useful when formalizing programming languages where bound names may become free during execution ("extrusion"), common in process calculi. It inherits the generic definition of permutations and support, and associated lemmas, from the Nominal approach, and the ability to stay close to pencil-and-paper proofs from the locally nameless approach. We explain how to use cofinite quantification in this setting, show why reasoning about renaming is more important here than in languages without extrusion, and provide results about infinite support, necessary when reasoning about countable choice.
△ Less
Submitted 23 October, 2017;
originally announced October 2017.
-
Coexistence of bulk and surface states probed by Shubnikov-de Haas oscillations in Bi$_2$Se$_3$ with high charge-carrier density
Authors:
E. K. de Vries,
S. Pezzini,
M. J. Meijer,
N. Koirala,
M. Salehi,
J. Moon,
S. Oh,
S. Wiedmann,
T. Banerjee
Abstract:
Topological insulators are ideally represented as having an insulating bulk with topologically protected, spin-textured surface states. However, it is increasingly becoming clear that these surface transport channels can be accompanied by a finite conducting bulk, as well as additional topologically trivial surface states. To investigate these parallel conduction transport channels, we studied Shu…
▽ More
Topological insulators are ideally represented as having an insulating bulk with topologically protected, spin-textured surface states. However, it is increasingly becoming clear that these surface transport channels can be accompanied by a finite conducting bulk, as well as additional topologically trivial surface states. To investigate these parallel conduction transport channels, we studied Shubnikov-de Haas oscillations in Bi$_2$Se$_3$ thin films, in high magnetic fields up to 30 T so as to access channels with a lower mobility. We identify a clear Zeeman-split bulk contribution to the oscillations from a comparison between the charge-carrier densities extracted from the magnetoresistance and the oscillations. Furthermore, our analyses indicate the presence of a two-dimensional state and signatures of additional states the origin of which cannot be conclusively determined. Our findings underpin the necessity of theoretical studies on the origin of and the interplay between these parallel conduction channels for a careful analysis of the material's performance.
△ Less
Submitted 27 July, 2017;
originally announced July 2017.
-
Towards the understanding of the origin of charge-current-induced spin voltage signals in the topological insulator Bi$_2$Se$_3$
Authors:
E. K. de Vries,
A. M. Kamerbeek,
N. Koirala,
M. Brahlek,
M. Salehi,
S. Oh,
B. J. van Wees,
T. Banerjee
Abstract:
Topological insulators provide a new platform for spintronics due to the spin texture of the surface states that are topologically robust against elastic backscattering. Here, we report on an investigation of the measured voltage obtained from efforts to electrically probe spin-momentum locking in the topological insulator Bi$_2$Se$_3$ using ferromagnetic contacts. Upon inverting the magnetization…
▽ More
Topological insulators provide a new platform for spintronics due to the spin texture of the surface states that are topologically robust against elastic backscattering. Here, we report on an investigation of the measured voltage obtained from efforts to electrically probe spin-momentum locking in the topological insulator Bi$_2$Se$_3$ using ferromagnetic contacts. Upon inverting the magnetization of the ferromagnetic contacts, we find a reversal of the measured voltage. Extensive analysis of the bias and temperature dependence of this voltage was done, considering the orientation of the magnetization relative to the current. Our findings indicate that the measured voltage can arise due to fringe-field-induced Hall voltages, different from current-induced spin polarization of the surface state charge carriers, as reported recently. Understanding the nontrivial origin of the measured voltage is important for realizing spintronic devices with topological insulators.
△ Less
Submitted 4 November, 2015; v1 submitted 28 October, 2015;
originally announced October 2015.
-
Supercharges, Quantum States and Angular Momentum for N=4 Supersymmetric Monopoles
Authors:
Erik Jan de Vries,
Bernd J. Schroers
Abstract:
We revisit the moduli space approximation to the quantum mechanics of monopoles in N=4 supersymmetric Yang-Mills-Higgs theory with maximal symmetry breaking. Starting with the observation that the set of fermionic zero-modes in N=4 supersymmetric Yang-Mills-Higgs theory can be viewed as two copies of the set of fermionic zero-modes in the N=2 version, we build a model to describe the quantum mecha…
▽ More
We revisit the moduli space approximation to the quantum mechanics of monopoles in N=4 supersymmetric Yang-Mills-Higgs theory with maximal symmetry breaking. Starting with the observation that the set of fermionic zero-modes in N=4 supersymmetric Yang-Mills-Higgs theory can be viewed as two copies of the set of fermionic zero-modes in the N=2 version, we build a model to describe the quantum mechanics of N=4 supersymmetric monopoles, based on our previous paper [1] on the N=2 case, in which this doubling of fermionic zero-modes is manifest throughout. Our final picture extends the familiar result that quantum states are described by differential forms on the moduli space and that the Hamiltonian operator is the Laplacian acting on forms. In particular, we derive a general expression for the total angular momentum operator on the moduli space which differs from the naive candidate by the adjoint action of the complex structures. We also express all the supercharges in terms of (twisted) Dolbeault operators and illustrate our results by discussing, in some detail, the N=4 supersymmetric quantum dynamics of monopoles in a theory with gauge group SU(3) broken to U(1) x U(1).
△ Less
Submitted 20 May, 2010; v1 submitted 4 April, 2010;
originally announced April 2010.
-
Uniqueness Ty** for Resource Management in Message-Passing Concurrency
Authors:
Edsko de Vries,
Adrian Francalanza,
Matthew Hennessy
Abstract:
We view channels as the main form of resources in a message-passing programming paradigm. These channels need to be carefully managed in settings where resources are scarce. To study this problem, we extend the pi-calculus with primitives for channel allocation and deallocation and allow channels to be reused to communicate values of different types. Inevitably, the added expressiveness increas…
▽ More
We view channels as the main form of resources in a message-passing programming paradigm. These channels need to be carefully managed in settings where resources are scarce. To study this problem, we extend the pi-calculus with primitives for channel allocation and deallocation and allow channels to be reused to communicate values of different types. Inevitably, the added expressiveness increases the possibilities for runtime errors. We define a substructural type system which combines uniqueness ty** and affine ty** to reject these ill-behaved programs.
△ Less
Submitted 29 March, 2010;
originally announced March 2010.
-
Supersymmetric Quantum Mechanics of Magnetic Monopoles: A Case Study
Authors:
Erik Jan de Vries,
Bernd J. Schroers
Abstract:
We study, in detail, the supersymmetric quantum mechanics of charge-(1,1) monopoles in N=2 supersymmetric Yang-Mills-Higgs theory with gauge group SU(3) spontaneously broken to U(1) x U(1). We use the moduli space approximation of the quantised dynamics, which can be expressed in two equivalent formalisms: either one describes quantum states by Dirac spinors on the moduli space, in which case th…
▽ More
We study, in detail, the supersymmetric quantum mechanics of charge-(1,1) monopoles in N=2 supersymmetric Yang-Mills-Higgs theory with gauge group SU(3) spontaneously broken to U(1) x U(1). We use the moduli space approximation of the quantised dynamics, which can be expressed in two equivalent formalisms: either one describes quantum states by Dirac spinors on the moduli space, in which case the Hamiltonian is the square of the Dirac operator, or one works with anti-holomorphic forms on the moduli space, in which case the Hamiltonian is the Laplacian acting on forms. We review the derivation of both formalisms, explicitly exhibit their equivalence and derive general expressions for the supercharges as differential operators in both formalisms. We propose a general expression for the total angular momentum operator as a differential operator, and check its commutation relations with the supercharges. Using the known metric structure of the moduli space of charge-(1,1) monopoles we show that there are no quantum bound states of such monopoles in the moduli space approximation. We exhibit scattering states and compute corresponding differential cross sections.
△ Less
Submitted 4 February, 2009; v1 submitted 13 November, 2008;
originally announced November 2008.
