Showing 1–15 of 15 results for author: Brady, E

Fluorine Abundances in Local Stellar Populations

Authors: K. E. Brady, C. A. Pilachowski, V. Grisoni, Z. G. Maas, K. A. Nault

Abstract: We present the first fluorine measurements in 12 normal giants belonging to the Galactic thin and thick disks using spectra obtained with the Phoenix infrared spectrometer on the 2.1m telescope at Kitt Peak. Abundances are determined from the (1-0) R9 2.3358 micron feature of the molecule HF. Additionally, sodium abundances are derived in 25 giants in the thin disk, thick disk, and halo using the… ▽ More We present the first fluorine measurements in 12 normal giants belonging to the Galactic thin and thick disks using spectra obtained with the Phoenix infrared spectrometer on the 2.1m telescope at Kitt Peak. Abundances are determined from the (1-0) R9 2.3358 micron feature of the molecule HF. Additionally, sodium abundances are derived in 25 giants in the thin disk, thick disk, and halo using the Na I line at 2.3379 microns. We report fluorine abundances for thin and thick disk stars in the metallicity range -0.7 < [Fe/H] < 0. We add two abundance measurements for stars with [Fe/H] < 0.5 dex which are at a critical metallicity range to constrain models. We find a larger dispersion in fluorine abundances than sodium abundances despite both species having similar overall uncertainties due to atmospheric parameters, suggesting this dispersion is real and not observational. The dispersion is slightly larger in the thick disk than the thin. The thin and thick disk average [F/Fe] for our sample of stars combined with the literature differ by 0.03 dex. The observations are compared to available chemical evolution models. △ Less

Submitted 4 June, 2024; originally announced June 2024.

Journal ref: AJ, 167, 291. 2024

M67 Blue Stragglers with High-resolution Infrared Spectroscopy

Authors: K. E. Brady, C. Sneden, C. A. Pilachowski, Melike Afşar, G. N. Mace, D. T. Jaffe, N. M. Gosnell, R. Seifert

Abstract: We report on the first detailed infrared chemical analysis of five binary members (S277, S997, S975, S1031, and S1195) in the open cluster M67 (NGC 2682). These stars are located outside (bluer and/or brighter than) the main-sequence turnoff region in M67. High-resolution (R ~ 45,000) near-infrared spectra were obtained with the Immersion GRating INfrared Spectrograph (IGRINS) at the McDonald Obse… ▽ More We report on the first detailed infrared chemical analysis of five binary members (S277, S997, S975, S1031, and S1195) in the open cluster M67 (NGC 2682). These stars are located outside (bluer and/or brighter than) the main-sequence turnoff region in M67. High-resolution (R ~ 45,000) near-infrared spectra were obtained with the Immersion GRating INfrared Spectrograph (IGRINS) at the McDonald Observatory 2.7 m Harlan J. Smith Telescope, providing full spectral coverage of the H and K bands. The abundances of C, Na, Mg, Al, Si, S, Ca, Fe, and Ni are measured using neutral atomic absorption lines. We detect v sin i greater than or equal to 25 km s-1 in three of our program stars: S1031, S975, and S1195. We find our derived abundances to be in good agreement with turnoff star abundances, similar to published analyses of blue straggler stars in M67 from optical spectra. Detection of a carbon enhancement or depletion resulting from mass transfer is difficult due to the uncertainties in the carbon abundance and the relatively modest changes that may occur through red giant and asymptotic giant branch evolution. △ Less

Submitted 28 September, 2023; originally announced September 2023.

Journal ref: AJ, 166, 154. 2023

A Democratic Platform for Engaging with Disabled Community in Generative AI Development

Authors: Deepak Giri, Erin Brady

Abstract: Artificial Intelligence (AI) systems, especially generative AI technologies are becoming more relevant in our society. Tools like ChatGPT are being used by members of the disabled community e.g., Autistic people may use it to help compose emails. The growing impact and popularity of generative AI tools have prompted us to examine their relevance within the disabled community. The design and develo… ▽ More Artificial Intelligence (AI) systems, especially generative AI technologies are becoming more relevant in our society. Tools like ChatGPT are being used by members of the disabled community e.g., Autistic people may use it to help compose emails. The growing impact and popularity of generative AI tools have prompted us to examine their relevance within the disabled community. The design and development phases often neglect this marginalized group, leading to inaccurate predictions and unfair discrimination directed towards them. This could result from bias in data sets, algorithms, and systems at various phases of creation and implementation. This workshop paper proposes a platform to involve the disabled community while building generative AI systems. With this platform, our aim is to gain insight into the factors that contribute to bias in the outputs generated by generative AI when used by the disabled community. Furthermore, we expect to comprehend which algorithmic factors are the main contributors to the output's incorrectness or irrelevancy. The proposed platform calls on both disabled and non-disabled people from various geographical and cultural backgrounds to collaborate asynchronously and remotely in a democratic approach to decision-making. △ Less

Submitted 26 September, 2023; originally announced September 2023.

ACM Class: I.2

Explicit Semiclassical Resonances from Many Delta Functions

Authors: Ethan J. Brady

Abstract: We study the scattering resonances arising from multiple $h$-dependent Dirac delta functions on the real line in the semiclassical regime $h \rightarrow 0$. We focus on resonances lying in strings along curves of the form $\text{Im } z \sim -γh\log(1/h)$ and find that resonances along such strings exist if and only if $γ$ is a slope of a Newton polygon we construct from the parameters. Furthermore… ▽ More We study the scattering resonances arising from multiple $h$-dependent Dirac delta functions on the real line in the semiclassical regime $h \rightarrow 0$. We focus on resonances lying in strings along curves of the form $\text{Im } z \sim -γh\log(1/h)$ and find that resonances along such strings exist if and only if $γ$ is a slope of a Newton polygon we construct from the parameters. Furthermore, the set of these $γ$ corresponds to a complete and disjoint partitioning of a line segment with delta functions at interval endpoints. Hence, there are at most $N-1$ strings of resonances from $N$ delta functions, improving a bound from (Datchev, Marzuola, & Wunsch 2023). Lastly, we identify a 'dominant pair' of delta functions in the sense that they correspond to the longest-living string of resonances, this string is the only one of logarithmic shape with respect to $\text{Re } z$, and no delta functions between them can contribute to strings of resonances. The simple properties of delta functions permit elementary proofs, requiring just undergraduate analysis and linear algebra. △ Less

Submitted 18 September, 2023; originally announced September 2023.

Comments: 31 pages, 9 figures

MSC Class: 35P25 (Primary) 47A40; 81U15; 58J50 (Secondary)

GRFolres: A code for modified gravity simulations in strong gravity

Authors: Llibert Aresté Saló, Sam E. Brady, Katy Clough, Daniela Doneva, Tamara Evstafyeva, Pau Figueras, Tiago França, Lorenzo Rossi, Shunhui Yao

Abstract: GRFolres is an open-source code for performing simulations in modified theories of gravity, based on the publicly available 3+1D numerical relativity code GRChombo. Note: Submitted for review in the Journal of Open Source Software; Comments welcome; The code can be found at https://github.com/GRChombo/GRFolres GRFolres is an open-source code for performing simulations in modified theories of gravity, based on the publicly available 3+1D numerical relativity code GRChombo. Note: Submitted for review in the Journal of Open Source Software; Comments welcome; The code can be found at https://github.com/GRChombo/GRFolres △ Less

Submitted 13 September, 2023; v1 submitted 12 September, 2023; originally announced September 2023.

Journal ref: J.Open Source Softw. 9 (2024) 98, 6369

Solving the initial conditions problem for modified gravity theories

Authors: Sam E. Brady, Llibert Aresté Saló, Katy Clough, Pau Figueras, Annamalai P. S

Abstract: Modified gravity theories such as Einstein scalar Gauss Bonnet (EsGB) contain higher derivative terms in the spacetime curvature in their action, which results in modifications to the Hamiltonian and momentum constraints of the theory. In principle, such modifications may affect the principal part of the operator in the resulting elliptic equations, and so further complicate the already highly non… ▽ More Modified gravity theories such as Einstein scalar Gauss Bonnet (EsGB) contain higher derivative terms in the spacetime curvature in their action, which results in modifications to the Hamiltonian and momentum constraints of the theory. In principle, such modifications may affect the principal part of the operator in the resulting elliptic equations, and so further complicate the already highly non-linear, coupled constraints that apply to the initial data in numerical relativity simulations of curved spacetimes. However, since these are effective field theories, we expect the additional curvature terms to be small, which motivates treating them simply as an additional source in the constraints, and iterating to find a solution to the full problem. In this work we implement and test a modification to the CTT/CTTK methods of solving the constraints for the case of the most general four derivative, parity invariant scalar-tensor theory, and show that solutions can be found in both asymptotically flat/black hole and periodic/cosmological spacetimes, even up to couplings of order unity in the theory. Such methods will allow for numerical investigations of a much broader class of initial data than has previously been possible in these theories, and should be straightforward to extend to similar models in the Horndeski class. △ Less

Submitted 30 November, 2023; v1 submitted 31 August, 2023; originally announced August 2023.

Comments: 9 pages, 4 figures, comments welcome!

GRDzhadzha: A code for evolving relativistic matter on analytic metric backgrounds

Authors: Josu C. Aurrekoetxea, Jamie Bamber, Sam E. Brady, Katy Clough, Thomas Helfer, James Marsden, Dina Traykova, Zipeng Wang

Abstract: GRDzhadzha is an open-source code for relativistic simulations of matter fields on curved spacetimes that admit an analytic description (e.g. stationary black holes). It is based on the publicly available 3+1D numerical relativity code GRChombo. Such a description is valid where the density of the matter is small compared to the curvature scale of the spacetime, which is the case for many physical… ▽ More GRDzhadzha is an open-source code for relativistic simulations of matter fields on curved spacetimes that admit an analytic description (e.g. stationary black holes). It is based on the publicly available 3+1D numerical relativity code GRChombo. Such a description is valid where the density of the matter is small compared to the curvature scale of the spacetime, which is the case for many physical scenarios - for example, dark matter environments. The approach offers significant savings on memory and speed compared to running full numerical relativity simulations, since the metric variables and their derivatives are calculated analytically, and therefore are not evolved or stored on the grid. This brief paper introduces the code and gives details of some applications for which it has already been used. △ Less

Submitted 16 August, 2023; originally announced August 2023.

Comments: Submitted for review in the Journal of Open Source Software; Comments welcome; The code can be found at https://github.com/GRChombo/GRDzhadzha.git

Frex: dependently-typed algebraic simplification

Authors: Guillaume Allais, Edwin Brady, Nathan Corbyn, Ohad Kammar, Jeremy Yallop

Abstract: We present an extensible, mathematically-structured algebraic simplification library design. We structure the library using universal algebraic concepts: a free algebra -- fral -- and a free extension -- frex -- of an algebra by a set of variables. The library's dependently-typed API guarantees simplification modules, even user-defined ones, are terminating, sound, and complete with respect to a w… ▽ More We present an extensible, mathematically-structured algebraic simplification library design. We structure the library using universal algebraic concepts: a free algebra -- fral -- and a free extension -- frex -- of an algebra by a set of variables. The library's dependently-typed API guarantees simplification modules, even user-defined ones, are terminating, sound, and complete with respect to a well-specified class of equations. Completeness offers intangible benefits in practice -- our main contribution is the novel design. Cleanly separating between the interface and implementation of simplification modules provides two new modularity axes. First, simplification modules share thousands of lines of infrastructure code dealing with term-representation, pretty-printing, certification, and macros/reflection. Second, new simplification modules can reuse existing ones. We demonstrate this design by develo** simplification modules for monoid varieties: ordinary, commutative, and involutive. We implemented this design in the new Idris2 dependently-typed programming language, and in Agda. △ Less

Submitted 27 June, 2023; originally announced June 2023.

Exploring outlooks towards generative AI-based assistive technologies for people with Autism

Authors: Deepak Giri, Erin Brady

Abstract: The last few years have significantly increased global interest in generative artificial intelligence. Deepfakes, which are synthetically created videos, emerged as an application of generative artificial intelligence. Fake news and pornographic content have been the two most prevalent negative use cases of deepfakes in the digital ecosystem. Deepfakes have some advantageous applications that expe… ▽ More The last few years have significantly increased global interest in generative artificial intelligence. Deepfakes, which are synthetically created videos, emerged as an application of generative artificial intelligence. Fake news and pornographic content have been the two most prevalent negative use cases of deepfakes in the digital ecosystem. Deepfakes have some advantageous applications that experts in the subject have thought of in the areas of filmmaking, teaching, etc. Research on the potential of deepfakes among people with disabilities is, however, scarce or nonexistent. This workshop paper explores the potential of deepfakes as an assistive technology. We examined Reddit conversations regarding Nvdia's new videoconferencing feature which allows participants to maintain eye contact during online meetings. Through manual web scra** and qualitative coding, we found 162 relevant comments discussing the relevance and appropriateness of the technology for people with Autism. The themes identified from the qualitative codes indicate a number of concerns for technology among the autistic community. We suggest that develo** generative AI-based assistive solutions will have ramifications for human-computer interaction (HCI), and present open questions that should be investigated further in this space. △ Less

Submitted 16 May, 2023; originally announced May 2023.

Comments: 6 pages, 1 figure

MSC Class: 68T07

Type Theory as a Language Workbench

Authors: Jan de Muijnck-Hughes, Guillaume Allais, Edwin Brady

Abstract: Language Workbenches offer language designers an expressive environment in which to create their DSLs. Similarly, research into mechanised meta-theory has shown how dependently typed languages provide expressive environments to formalise and study DSLs and their meta-theoretical properties. But can we claim that dependently typed languages qualify as language workbenches? We argue yes! We have d… ▽ More Language Workbenches offer language designers an expressive environment in which to create their DSLs. Similarly, research into mechanised meta-theory has shown how dependently typed languages provide expressive environments to formalise and study DSLs and their meta-theoretical properties. But can we claim that dependently typed languages qualify as language workbenches? We argue yes! We have developed an exemplar DSL called Velo that showcases not only dependently typed techniques to realise and manipulate IRs, but that dependently typed languages make fine language workbenches. Velo is a simple verified language with well-typed holes and comes with a complete compiler pipeline: parser, elaborator, REPL, evaluator, and compiler passes. Specifically, we describe our design choices for well-typed IRs design that includes support for well-typed holes, how CSE is achieved in a well-typed setting, and how the mechanised type-soundness proof for Velo is the source of the evaluator. △ Less

Submitted 30 January, 2023; originally announced January 2023.

Comments: 18 pages, Accepted for publication at ECVS

ACM Class: F.3.1; F.3.2; D.3.1; D.3.3

Model-assisted deep learning of rare extreme events from partial observations

Authors: Anna Asch, Ethan Brady, Hugo Gallardo, John Hood, Bryan Chu, Mohammad Farazmand

Abstract: To predict rare extreme events using deep neural networks, one encounters the so-called small data problem because even long-term observations often contain few extreme events. Here, we investigate a model-assisted framework where the training data is obtained from numerical simulations, as opposed to observations, with adequate samples from extreme events. However, to ensure the trained networks… ▽ More To predict rare extreme events using deep neural networks, one encounters the so-called small data problem because even long-term observations often contain few extreme events. Here, we investigate a model-assisted framework where the training data is obtained from numerical simulations, as opposed to observations, with adequate samples from extreme events. However, to ensure the trained networks are applicable in practice, the training is not performed on the full simulation data; instead we only use a small subset of observable quantities which can be measured in practice. We investigate the feasibility of this model-assisted framework on three different dynamical systems (Rossler attractor, FitzHugh-Nagumo model, and a turbulent fluid flow) and three different deep neural network architectures (feedforward, long short-term memory, and reservoir computing). In each case, we study the prediction accuracy, robustness to noise, reproducibility under repeated training, and sensitivity to the type of input data. In particular, we find long short-term memory networks to be most robust to noise and to yield relatively accurate predictions, while requiring minimal fine-tuning of the hyperparameters. △ Less

Submitted 22 March, 2022; v1 submitted 4 November, 2021; originally announced November 2021.

Comments: Accepted for publication in Chaos: An Interdisciplinary Journal of Nonlinear Science

Idris 2: Quantitative Type Theory in Practice

Authors: Edwin Brady

Abstract: Dependent types allow us to express precisely what a function is intended to do. Recent work on Quantitative Type Theory (QTT) extends dependent type systems with linearity, also allowing precision in expressing when a function can run. This is promising, because it suggests the ability to design and reason about resource usage protocols, such as we might find in distributed and concurrent program… ▽ More Dependent types allow us to express precisely what a function is intended to do. Recent work on Quantitative Type Theory (QTT) extends dependent type systems with linearity, also allowing precision in expressing when a function can run. This is promising, because it suggests the ability to design and reason about resource usage protocols, such as we might find in distributed and concurrent programming, where the state of a communication channel changes throughout program execution. As yet, however, there has not been a full-scale programming language with which to experiment with these ideas. Idris 2 is a new version of the dependently typed language Idris, with a new core language based on QTT, supporting linear and dependent types. In this paper, we introduce Idris 2, and describe how QTT has influenced its design. We give examples of the benefits of QTT in practice including: expressing which data is erased at run time, at the type level; and, resource tracking in the type system leading to type-safe concurrent programming with session types. △ Less

Submitted 1 April, 2021; originally announced April 2021.

Comments: To appear in proceedings of ECOOP 2021

Value-Dependent Session Design in a Dependently Typed Language

Authors: Jan de Muijnck-Hughes, Edwin Brady, Wim Vanderbauwhede

Abstract: Session Types offer a ty** discipline that allows protocol specifications to be used during type-checking, ensuring that implementations adhere to a given specification. When looking to realise global session types in a dependently typed language care must be taken that values introduced in the description are used by roles that know about the value. We present Sessions, a Resource Dependent E… ▽ More Session Types offer a ty** discipline that allows protocol specifications to be used during type-checking, ensuring that implementations adhere to a given specification. When looking to realise global session types in a dependently typed language care must be taken that values introduced in the description are used by roles that know about the value. We present Sessions, a Resource Dependent EDSL for describing global session descriptions in the dependently typed language Idris. As we construct session descriptions the values parameterising the EDSLs' type keeps track of roles and messages they have encountered. We can use this knowledge to ensure that message values are only used by those who know the value. Sessions supports protocol descriptions that are computable, composable, higher-order, and value-dependent. We demonstrate Sessions expressiveness by describing the TCP Handshake, a multi-modal server providing echo and basic arithmetic operations, and a Higher-Order protocol that supports an authentication interaction step. △ Less

Submitted 2 April, 2019; originally announced April 2019.

Comments: In Proceedings PLACES 2019, arXiv:1904.00396

Journal ref: EPTCS 291, 2019, pp. 47-59

Sequential decision problems, dependent types and generic solutions

Authors: Nicola Botta, Patrik Jansson, Cezar Ionescu, David R. Christiansen, Edwin Brady

Abstract: We present a computer-checked generic implementation for solving finite-horizon sequential decision problems. This is a wide class of problems, including inter-temporal optimizations, knapsack, optimal bracketing, scheduling, etc. The implementation can handle time-step dependent control and state spaces, and monadic representations of uncertainty (such as stochastic, non-deterministic, fuzzy, or… ▽ More We present a computer-checked generic implementation for solving finite-horizon sequential decision problems. This is a wide class of problems, including inter-temporal optimizations, knapsack, optimal bracketing, scheduling, etc. The implementation can handle time-step dependent control and state spaces, and monadic representations of uncertainty (such as stochastic, non-deterministic, fuzzy, or combinations thereof). This level of genericity is achievable in a programming language with dependent types (we have used both Idris and Agda). Dependent types are also the means that allow us to obtain a formalization and computer-checked proof of the central component of our implementation: Bellman's principle of optimality and the associated backwards induction algorithm. The formalization clarifies certain aspects of backwards induction and, by making explicit notions such as viability and reachability, can serve as a starting point for a theory of controllability of monadic dynamical systems, commonly encountered in, e.g., climate impact research. △ Less

Submitted 22 March, 2017; v1 submitted 23 October, 2016; originally announced October 2016.

Comments: 23 pages, 2 figures

Journal ref: Logical Methods in Computer Science, Volume 13, Issue 1 (March 17, 2017) lmcs:3191

HackAttack: Game-Theoretic Analysis of Realistic Cyber Conflicts

Authors: Erik M. Ferragut, Andrew C. Brady, Ethan J. Brady, Jacob M. Ferragut, Nathan M. Ferragut, Max C. Wildgruber

Abstract: Game theory is appropriate for studying cyber conflict because it allows for an intelligent and goal-driven adversary. Applications of game theory have led to a number of results regarding optimal attack and defense strategies. However, the overwhelming majority of applications explore overly simplistic games, often ones in which each participant's actions are visible to every other participant. T… ▽ More Game theory is appropriate for studying cyber conflict because it allows for an intelligent and goal-driven adversary. Applications of game theory have led to a number of results regarding optimal attack and defense strategies. However, the overwhelming majority of applications explore overly simplistic games, often ones in which each participant's actions are visible to every other participant. These simplifications strip away the fundamental properties of real cyber conflicts: probabilistic alerting, hidden actions, unknown opponent capabilities. In this paper, we demonstrate that it is possible to analyze a more realistic game, one in which different resources have different weaknesses, players have different exploits, and moves occur in secrecy, but they can be detected. Certainly, more advanced and complex games are possible, but the game presented here is more realistic than any other game we know of in the scientific literature. While optimal strategies can be found for simpler games using calculus, case-by-case analysis, or, for stochastic games, Q-learning, our more complex game is more naturally analyzed using the same methods used to study other complex games, such as checkers and chess. We define a simple evaluation function and ploy multi-step searches to create strategies. We show that such scenarios can be analyzed, and find that in cases of extreme uncertainty, it is often better to ignore one's opponent's possible moves. Furthermore, we show that a simple evaluation function in a complex game can lead to interesting and nuanced strategies. △ Less

Submitted 13 November, 2015; originally announced November 2015.

Comments: 8 pages