Showing 1–50 of 65 results for author: de Amorim, A

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.

Comments: Accepted to Logic in Computer Science (LICS) 2025. Comments welcome!

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.

Comments: 37 pages, 24 figures; Replaced to keep consistency with non-extended version of the paper to appear at PLDI 25

ACM Class: F.3.2; F.4.2

Cryptis: Cryptographic Reasoning in Separation Logic

Authors: Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi

Abstract: We introduce Cryptis, an extension of the Iris separation logic that can be used to verify cryptographic components using the symbolic model of cryptography. The combination of separation logic and cryptographic reasoning allows us to prove the correctness of a protocol and later reuse this result to verify larger systems that rely on the protocol. To make this integration possible, we propose nov… ▽ More We introduce Cryptis, an extension of the Iris separation logic that can be used to verify cryptographic components using the symbolic model of cryptography. The combination of separation logic and cryptographic reasoning allows us to prove the correctness of a protocol and later reuse this result to verify larger systems that rely on the protocol. To make this integration possible, we propose novel specifications for authentication protocols that allow agents in a network to agree on the use of system resources. We evaluate our approach by verifying various authentication protocols and a key-value store server that uses these authentication protocols to connect to clients. Our results are formalized in Coq. △ Less

Submitted 28 February, 2025; originally announced February 2025.

Kleene algebra with commutativity conditions is undecidable

Authors: Arthur Azevedo de Amorim, Cheng Zhang, Marco Gaboardi

Abstract: We prove that the equational theory of Kleene algebra with commutativity conditions on primitives (or atomic terms) is undecidable, thereby settling a longstanding open question in the theory of Kleene algebra. While this question has also been recently solved independently by Kuznetsov, our results hold even for weaker theories that do not support the induction axioms of Kleene algebra. We prove that the equational theory of Kleene algebra with commutativity conditions on primitives (or atomic terms) is undecidable, thereby settling a longstanding open question in the theory of Kleene algebra. While this question has also been recently solved independently by Kuznetsov, our results hold even for weaker theories that do not support the induction axioms of Kleene algebra. △ Less

Submitted 24 November, 2024; originally announced November 2024.

Comments: Published at CSL 2025

Domain Reasoning in TopKAT

Authors: Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi

Abstract: TopKAT is the algebraic theory of Kleene algebra with tests (KAT) extended with a top element. Compared to KAT, one pleasant feature of TopKAT is that, in relational models, the top element allows us to express the domain and codomain of a relation. This enables several applications in program logics, such as proving under-approximate specifications or reachability properties of imperative program… ▽ More TopKAT is the algebraic theory of Kleene algebra with tests (KAT) extended with a top element. Compared to KAT, one pleasant feature of TopKAT is that, in relational models, the top element allows us to express the domain and codomain of a relation. This enables several applications in program logics, such as proving under-approximate specifications or reachability properties of imperative programs. However, while TopKAT inherits many pleasant features of KATs, such as having a decidable equational theory, it is incomplete with respect to relational models. In other words, there are properties that hold true of all relational TopKATs but cannot be proved with the axioms of TopKAT. This issue is potentially worrisome for program-logic applications, in which relational models play a key role. In this paper, we further investigate the completeness properties of TopKAT with respect to relational models. We show that TopKAT is complete with respect to (co)domain comparison of KAT terms, but incomplete when comparing the (co)domain of arbitrary TopKAT terms. Since the encoding of under-approximate specifications in TopKAT hinges on this type of formula, the aforementioned incompleteness results have a limited impact when using TopKAT to reason about such specifications. △ Less

Submitted 29 April, 2024; originally announced April 2024.

Comments: A version of this article is accepted at ICALP 2024

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.

SECOMP: Formally Secure Compilation of Compartmentalized C Programs

Authors: Jérémy Thibault, Roberto Blanco, Dongjae Lee, Sven Argo, Arthur Azevedo de Amorim, Aïna Linn Georges, Catalin Hritcu, Andrew Tolmach

Abstract: Undefined behavior in C often causes devastating security vulnerabilities. One practical mitigation is compartmentalization, which allows developers to structure large programs into mutually distrustful compartments with clearly specified privileges and interactions. In this paper we introduce SECOMP, a compiler for compartmentalized C code that comes with machine-checked proofs guaranteeing that… ▽ More Undefined behavior in C often causes devastating security vulnerabilities. One practical mitigation is compartmentalization, which allows developers to structure large programs into mutually distrustful compartments with clearly specified privileges and interactions. In this paper we introduce SECOMP, a compiler for compartmentalized C code that comes with machine-checked proofs guaranteeing that the scope of undefined behavior is restricted to the compartments that encounter it and become dynamically compromised. These guarantees are formalized as the preservation of safety properties against adversarial contexts, a secure compilation criterion similar to full abstraction, and this is the first time such a strong criterion is proven for a mainstream programming language. To achieve this we extend the languages of the CompCert verified C compiler with isolated compartments that can only interact via procedure calls and returns, as specified by cross-compartment interfaces. We adapt the passes and optimizations of CompCert as well as their correctness proofs to this compartment-aware setting. We then use compiler correctness as an ingredient in a larger secure compilation proof that involves several proof engineering novelties, needed to scale formally secure compilation up to a C compiler. △ Less

Submitted 1 January, 2025; v1 submitted 29 January, 2024; originally announced January 2024.

Comments: CCS'24 version, slightly updated and extended with appendices and a few more references

Pipelines and Beyond: Graph Types for ADTs with Futures

Authors: Francis Rinaldi, june wunder, Arthur Aevedo De Amorim, Stefan K. Muller

Abstract: Parallel programs are frequently modeled as dependency or cost graphs, which can be used to detect various bugs, or simply to visualize the parallel structure of the code. However, such graphs reflect just one particular execution and are typically constructed in a post-hoc manner. Graph types, which were introduced recently to mitigate this problem, can be assigned statically to a program by a ty… ▽ More Parallel programs are frequently modeled as dependency or cost graphs, which can be used to detect various bugs, or simply to visualize the parallel structure of the code. However, such graphs reflect just one particular execution and are typically constructed in a post-hoc manner. Graph types, which were introduced recently to mitigate this problem, can be assigned statically to a program by a type system and compactly represent the family of all graphs that could result from the program. Unfortunately, prior work is restricted in its treatment of futures, an increasingly common and especially dynamic form of parallelism. In short, each instance of a future must be statically paired with a vertex name. Previously, this led to the restriction that futures could not be placed in collections or be used to construct data structures. Doing so is not a niche exercise: such structures form the basis of numerous algorithms that use forms of pipelining to achieve performance not attainable without futures. All but the most limited of these examples are out of reach of prior graph type systems. In this paper, we propose a graph type system that allows for almost arbitrary combinations of futures and recursive data types. We do so by indexing datatypes with a type-level vertex structure, a codata structure that supplies unique vertex names to the futures in a data structure. We prove the soundness of the system in a parallel core calculus annotated with vertex structures and associated operations. Although the calculus is annotated, this is merely for convenience in defining the type system. We prove that it is possible to annotate arbitrary recursive types with vertex structures, and show using a prototype inference engine that these annotations can be inferred from OCaml-like source code for several complex parallel algorithms. △ Less

Submitted 12 November, 2023; originally announced November 2023.

Comments: 65 pages, 41 figures, submitted to POPL 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.

Comments: Extended version of PLDI '23 paper

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.

The miniJPAS survey: The galaxy populations in the most massive cluster in miniJPAS, mJPC2470-1771

Authors: J. E. Rodríguez Martín, R. M. González Delgado, G. Martínez-Solaeche, L. A. Díaz-García, A. de Amorim, R. García-Benito, E. Pérez, R. Cid Fernandes, E. R. Carrasco, M. Maturi, A. Finoguenov, P. A. A. Lopes, A. Cortesi, G. Lucatelli, J. M. Diego, A. L. Chies-Santos, R. A. Dupke, Y. Jiménez-Teja, J. M. Vílchez, L. R. Abramo, J. Alcaniz, N. Benítez, S. Bonoli, A. J. Cenarro, D. Cristóbal-Hornillos , et al. (11 additional authors not shown)

Abstract: The miniJPAS is a 1 deg$^2$ survey that uses the Javalambre-Physics of the Accelerating Universe Astrophysical Survey (J-PAS) filter system (54 narrow-band filters) with the Pathfinder camera. We study mJPC2470-1771, the most massive cluster detected in miniJPAS. We study the stellar population properties of the members, their star formation rates (SFR), star formation histories (SFH), the emissio… ▽ More The miniJPAS is a 1 deg$^2$ survey that uses the Javalambre-Physics of the Accelerating Universe Astrophysical Survey (J-PAS) filter system (54 narrow-band filters) with the Pathfinder camera. We study mJPC2470-1771, the most massive cluster detected in miniJPAS. We study the stellar population properties of the members, their star formation rates (SFR), star formation histories (SFH), the emission line galaxy (ELG) population, their spatial distribution, and the effect of the environment on them, showing the power of J-PAS to study the role of environment in galaxy evolution. We use a spectral energy distribution (SED) fitting code to derive the stellar population properties of the galaxy members: stellar mass, extinction, metallicity, colours, ages, SFH (a delayed-$τ$ model), and SFRs. Artificial Neural Networks are used for the identification of the ELG population through the detection of H$α$, [NII], H$β$, and [OIII] nebular emission. We use the WHAN and BPT diagrams to separate them into star-forming galaxies and AGNs. We find that the fraction of red galaxies increases with the cluster-centric radius. We select 49 ELG, 65.3\% of the them are probably star forming galaxies, and they are dominated by blue galaxies. 24% are likely to host an AGN (Seyfert or LINER galaxies). The rest are difficult to classify and are most likely composite galaxies. Our results are compatible with an scenario where galaxy members were formed roughly at the same epoch, but blue galaxies have had more recent star formation episodes, and they are quenching from inside-out of the cluster centre. The spatial distribution of red galaxies and their properties suggest that they were quenched prior to the cluster accretion or an earlier cluster accretion epoch. AGN feedback and/or mass might also be intervening in the quenching of these galaxies. △ Less

Submitted 20 July, 2022; originally announced July 2022.

Comments: 24 pages, 17 figures, 4 tables, accepted in Astronomy & Astrophysics

Journal ref: A&A 666, A160 (2022)

On Pitts' Relational Properties of Domains

Authors: Arthur Azevedo de Amorim

Abstract: Andrew Pitts' framework of relational properties of domains is a powerful method for defining predicates or relations on domains, with applications ranging from reasoning principles for program equivalence to proofs of adequacy connecting denotational and operational semantics. Its main appeal is handling recursive definitions that are not obviously well-founded: as long as the corresponding domai… ▽ More Andrew Pitts' framework of relational properties of domains is a powerful method for defining predicates or relations on domains, with applications ranging from reasoning principles for program equivalence to proofs of adequacy connecting denotational and operational semantics. Its main appeal is handling recursive definitions that are not obviously well-founded: as long as the corresponding domain is also defined recursively, and its recursion pattern lines up appropriately with the definition of the relations, the framework can guarantee their existence. Pitts' original development used the Knaster-Tarski fixed-point theorem as a key ingredient. In these notes, I show how his construction can be seen as an instance of other key fixed-point theorems: the inverse limit construction, the Banach fixed-point theorem and the Kleene fixed-point theorem. The connection underscores how Pitts' construction is intimately tied to the methods for constructing the base recursive domains themselves, and also to techniques based on guarded recursion, or step-indexing, that have become popular in the last two decades. △ Less

Submitted 14 July, 2022; originally announced July 2022.

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.

The miniJPAS survey: The role of group environment in quenching the star formation

Authors: R. M. González Delgado, J. E. Rodríguez-Martín, L. A. Díaz-García, A. de Amorim, R. García-Benito, G. Martínez-Solaeche, P. A. A. Lopes, M. Maturi, E. Pérez, R. Cid Fernandes, A. Cortesi, A. Finoguenov, E. R. Carrasco, A. Hernán-Caballero, L. R. Abramo, J. Alcaniz, N. Benítez, S. Bonoli, A. J. Cenarro, D. Cristóbal-Hornillos, J. M. Diego, R. A. Dupke, A. Ederoclite, J. A. Fernández-Ontiveros, C. López-Sanjuan , et al. (10 additional authors not shown)

Abstract: The miniJPAS survey has observed $\sim 1$ deg$^2$ on the AEGIS field with 60 bands (spectral resolution of $R \sim 60$) in order to demonstrate the capabilities of the Javalambre-Physics of the Accelerating Universe Astrophysical Survey (J-PAS) that will map $\sim 8000$ deg$^2$ of the northern sky in the next years. This paper shows the power of J-PAS to detect low mass groups and characterise the… ▽ More The miniJPAS survey has observed $\sim 1$ deg$^2$ on the AEGIS field with 60 bands (spectral resolution of $R \sim 60$) in order to demonstrate the capabilities of the Javalambre-Physics of the Accelerating Universe Astrophysical Survey (J-PAS) that will map $\sim 8000$ deg$^2$ of the northern sky in the next years. This paper shows the power of J-PAS to detect low mass groups and characterise their galaxy populations up to $z \sim 1$. We use the spectral energy distribution fitting code BaySeAGal to derive the stellar population properties of the galaxy members in 80 groups at $z \leq 0.8$ previously detected by the AMICO code, as well as for a galaxy field sample retrieved from the whole miniJPAS sample. We identify blue, red, quiescent, and transition galaxy populations through their rest-frame (extinction corrected) colour, stellar mass ($M_\star$) and specific star formation rate. We measure their abundance as a function of $M_\star$ and environment. We find: (i) The fraction of red and quiescent galaxies in groups increases with $M_\star$ and it is always higher in groups than in the field. (ii) The quenched fraction excess (QFE) in groups strongly increases with $M_\star$, (from a few percent to higher than 60% in the mass range $10^{10} - 3 \times 10 ^{11}$ $M_\odot$. (iii) The abundance excess of transition galaxies in groups shows a modest dependence with $M_\star$ (iv) The fading time scale is very short ($<1.5$ Gyr), indicating that the star formation declines very rapidly in groups. (v) The evolution of the galaxy quenching rate in groups shows a modest but significant evolution since $z\sim0.8$, compatible with an evolution with constant $QFE=0.4$, previously measured for satellites in the nearby Universe, and consistent with a scenario where the low-mass star-forming galaxies in clusters at $z= 1-1.4$ are environmentally quenched. △ Less

Submitted 12 July, 2022; originally announced July 2022.

Comments: 21 pages, 20 figures, accepted for publication in Astronomy & Astrophysics

The miniJPAS survey: Identification and characterization of the emission line galaxies down to $z < 0.35$ in the AEGIS field

Authors: G. Martínez-Solaeche, R. M. González Delgado, R. García-Benito, L. A. Díaz-García, J. E. Rodríguez-Martín, E. Pérez, A. de Amorim, S. Duarte Puertas, Laerte Sodré Jr., David Sobral, Jonás Chaves-Montero, J. M. Vílchez, A. Hernán-Caballero, C. López-Sanjuan, A. Cortesi, S. Bonoli, A. J. Cenarro, R. A. Dupke, A. Marín-Franch, J. Varela, H. Vázquez Ramió, L. R. Abramo, D. Cristóbal-Hornillos, M. Moles, J. Alcaniz , et al. (6 additional authors not shown)

Abstract: The Javalambre-Physics of the Accelerating Universe Astrophysical Survey (J-PAS) is expected to map thousands of square degrees of the northern sky with 56 narrowband filters in the upcoming years. This will make J-PAS a very competitive and unbiased emission line survey compared to spectroscopic or narrowband surveys with fewer filters. The miniJPAS survey covered 1 deg$^2$, and it used the same… ▽ More The Javalambre-Physics of the Accelerating Universe Astrophysical Survey (J-PAS) is expected to map thousands of square degrees of the northern sky with 56 narrowband filters in the upcoming years. This will make J-PAS a very competitive and unbiased emission line survey compared to spectroscopic or narrowband surveys with fewer filters. The miniJPAS survey covered 1 deg$^2$, and it used the same photometric system as J-PAS, but the observations were carried out with the pathfinder J-PAS camera. In this work, we identify and characterize the sample of emission line galaxies (ELGs) from miniJPAS with a redshift lower than $0.35$. Using a method based on artificial neural networks, we detect the ELG population and measure the equivalent width and flux of the $Hα$, $Hβ$, [OIII], and [NII] emission lines. We explore the ionization mechanism using the diagrams [OIII]/H$β$ versus [NII]/H$α$ (BPT) and EW(H$α$) versus [NII]/H$α$ (WHAN). We identify 1787 ELGs ($83$%) from the parent sample (2154 galaxies) in the AEGIS field. For the galaxies with reliable EW values that can be placed in the WHAN diagram (2000 galaxies in total), we obtained that $72.8 \pm 0.4$%, $17.7 \pm 0.4$% , and $9.4 \pm 0.2$% are star-forming (SF), active galactic nucleus (Seyfert), and quiescent galaxies, respectively. Based on the flux of $Hα$ we find that the star formation main sequence is described as $\log$ SFR $[M_\mathrm{\odot} \mathrm{yr}^{-1}] = 0.90^{+ 0.02}_{-0.02} \log M_{\star} [M_\mathrm{\odot}] -8.85^{+ 0.19}_{-0.20}$ and has an intrinsic scatter of $0.20^{+ 0.01}_{-0.01}$. The cosmic evolution of the SFR density ($ρ_{\text{SFR}}$) is derived at three redshift bins: $0 < z \leq 0.15$, $0.15 < z \leq 0.25$, and $0.25 < z \leq 0.35$, which agrees with previous results that were based on measurements of the $Hα$ emission line. △ Less

Submitted 4 April, 2022; originally announced April 2022.

Comments: 22 pages, 19 figures

Journal ref: A&A 661, A99 (2022)

Bunched Fuzz: Sensitivity for Vector Metrics

Authors: june wunder, Arthur Azevedo de Amorim, Patrick Baillot, Marco Gaboardi

Abstract: Program sensitivity measures the distance between the outputs of a program when run on two related inputs. This notion, which plays a key role in areas such as data privacy and optimization, has been the focus of several program analysis techniques introduced in recent years. Among the most successful ones, we can highlight type systems inspired by linear logic, as pioneered by Reed and Pierce in… ▽ More Program sensitivity measures the distance between the outputs of a program when run on two related inputs. This notion, which plays a key role in areas such as data privacy and optimization, has been the focus of several program analysis techniques introduced in recent years. Among the most successful ones, we can highlight type systems inspired by linear logic, as pioneered by Reed and Pierce in the Fuzz programming language. In Fuzz, each type is equipped with its own distance, and sensitivity analysis boils down to type checking. In particular, Fuzz features two product types, corresponding to two different notions of distance: the tensor product combines the distances of each component by adding them, while the with product takes their maximum. In this work, we show that these products can be generalized to arbitrary $L^p$ distances, metrics that are often used in privacy and optimization. The original Fuzz products, tensor and with, correspond to the special cases $L^1$ and $L^\infty$. To ease the handling of such products, we extend the Fuzz type system with bunches -- as in the logic of bunched implications -- where the distances of different groups of variables can be combined using different $L^p$ distances. We show that our extension can be used to reason about quantitative properties of probabilistic programs. △ Less

Submitted 1 February, 2023; v1 submitted 3 February, 2022; originally announced February 2022.

The DIVING$^{3D}$ Survey -- Deep IFS View of Nuclei of Galaxies -- I. Definition and Sample Presentation

Authors: J. E. Steiner, R. B. Menezes, T. V. Ricci, Patrícia da Silva, R. Cid Fernandes, N. Vale Asari, M. S. Carvalho, D. May, Paula R. T. Coelho, A. L. de Amorim

Abstract: We present the Deep Integral Field Spectrograph View of Nuclei of Galaxies (DIVING$^{3D}$) survey, a seeing-limited optical 3D spectroscopy study of the central regions of all 170 galaxies in the Southern hemisphere with B < 12.0 and |b| > 15 degrees. Most of the observations were taken with the Integral Field Unit of the Gemini Multi-Object Spectrograph, at the Gemini South telescope, but some ar… ▽ More We present the Deep Integral Field Spectrograph View of Nuclei of Galaxies (DIVING$^{3D}$) survey, a seeing-limited optical 3D spectroscopy study of the central regions of all 170 galaxies in the Southern hemisphere with B < 12.0 and |b| > 15 degrees. Most of the observations were taken with the Integral Field Unit of the Gemini Multi-Object Spectrograph, at the Gemini South telescope, but some are also being taken with the Southern Astrophysical Research Telescope (SOAR) Integral Field Spectrograph. The DIVING$^{3D}$ survey was designed for the study of nuclear emission-line properties, circumnuclear (within scales of hundreds of pc) emission-line properties, stellar and gas kinematics and stellar archaeology. The data have a combination of high spatial and spectral resolution not matched by previous surveys and will result in significant contributions for studies related to, for example, the statistics of low-luminosity active galactic nuclei, the ionization mechanisms in Low-Ionization Nuclear Emission-Line Regions, the nature of transition objects, among other topics. △ Less

Submitted 31 January, 2022; originally announced February 2022.

Comments: 17 pages, 10 figures, 1 table, published in MNRAS

Journal ref: MNRAS, 510, 5780 (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.

Comments: Updated title. Accepted at FoSSaCS 2023

On Incorrectness Logic and Kleene Algebra with Top and Tests

Authors: Cheng Zhang, Arthur Azevedo de Amorim, Marco Gaboardi

Abstract: Kleene algebra with tests (KAT) is a foundational equational framework for reasoning about programs, which has found applications in program transformations, networking and compiler optimizations, among many other areas. In his seminal work, Kozen proved that KAT subsumes propositional Hoare logic, showing that one can reason about the (partial) correctness of while programs by means of the equati… ▽ More Kleene algebra with tests (KAT) is a foundational equational framework for reasoning about programs, which has found applications in program transformations, networking and compiler optimizations, among many other areas. In his seminal work, Kozen proved that KAT subsumes propositional Hoare logic, showing that one can reason about the (partial) correctness of while programs by means of the equational theory of KAT. In this work, we investigate the support that KAT provides for reasoning about incorrectness, instead, as embodied by Ohearn's recently proposed incorrectness logic. We show that KAT cannot directly express incorrectness logic. The main reason for this limitation can be traced to the fact that KAT cannot express explicitly the notion of codomain, which is essential to express incorrectness triples. To address this issue, we study Kleene Algebra with Top and Tests (TopKAT), an extension of KAT with a top element. We show that TopKAT is powerful enough to express a codomain operation, to express incorrectness triples, and to prove all the rules of incorrectness logic sound. This shows that one can reason about the incorrectness of while-like programs by means of the equational theory of TopKAT. △ Less

Submitted 4 August, 2022; v1 submitted 17 August, 2021; originally announced August 2021.

Journal ref: Proc. ACM Program. Lang. 6, POPL, Article 29 (January 2022), 30 pages (2022)

The Fornax Cluster through S-PLUS

Authors: A. V. Smith Castelli, C. Mendes de Oliveira, F. Herpich, C. E. Barbosa, C. Escudero, M. Grossi, L. Sodre, C. R. de Bom, L. Zenocratti, M. E. De Rossi, A. Cortesi, R. Cid Fernandes, A. R. Lopes, E. Telles, G. B. Oliveira Schwarz, M. L. L. Dantas, F. R. Faifer, A. Chies Santos, J. Saponara, V. Reynaldi, I. Andruchow, L. Sesto, M. F. Mestre, A. L. de Amorim, E. V. R. de Lima , et al. (3 additional authors not shown)

Abstract: The Southern Photometric Local Universe Survey (S-PLUS) aims to map $\approx$ 9300 deg$^2$ of the Southern sky using the Javalambre filter system of 12 optical bands, 5 Sloan-like filters and 7 narrow-band filters centered on several prominent stellar features ([OII], Ca H+K, D4000, H$_δ$, Mgb, H$_α$ and CaT). S-PLUS is carried out with the T80-South, a new robotic 0.826-m telescope located on CTI… ▽ More The Southern Photometric Local Universe Survey (S-PLUS) aims to map $\approx$ 9300 deg$^2$ of the Southern sky using the Javalambre filter system of 12 optical bands, 5 Sloan-like filters and 7 narrow-band filters centered on several prominent stellar features ([OII], Ca H+K, D4000, H$_δ$, Mgb, H$_α$ and CaT). S-PLUS is carried out with the T80-South, a new robotic 0.826-m telescope located on CTIO, equipped with a wide FoV camera (2 deg$^2$). In this poster we introduce project #59 of the S-PLUS collaboration aimed at studying the Fornax galaxy cluster covering an sky area of $\approx$ 11 $\times$ 7 deg$^2$, and with homogeneous photometry in the 12 optical bands of S-PLUS (Coordinator: A. Smith Castelli). △ Less

Submitted 15 April, 2021; originally announced April 2021.

Comments: 3 pages, 5 figures; accepted to be published in Boletín de la Asociación Argentina de Astronomía

The miniJPAS survey: Identification and characterization of galaxy populations with the J-PAS photometric system

Authors: R. M. González Delgado, L. A. Díaz-García, A. de Amorim, G. Bruzual, R. Cid Fernandes, E. Pérez, S. Bonoli, A. J. Cenarro, P. R. T. Coelho, A. Cortesi, R. García-Benito, R. López Fernández, G. Martínez-Solaeche, J. E. Rodríguez-Martín, G. Magris, A. Mejía-Narvaez, D. Brito-Silva, L. R. Abramo, J. M. Diego, R. A. Dupke, A. Hernán-Caballero, C. Hernández-Monteagudo, C. López-Sanjuan, A. Marín-Franch, V. Marra , et al. (17 additional authors not shown)

Abstract: J-PAS will soon start imaging 8000 deg2 of the northern sky with its unique set of 56 filters (R $\sim$ 60). Before, we observed 1 deg2 on the AEGIS field with an interim camera with all the J-PAS filters. With this data (miniJPAS), we aim at proving the scientific potential of J-PAS to identify and characterize the galaxy populations with the goal of performing galaxy evolution studies across cos… ▽ More J-PAS will soon start imaging 8000 deg2 of the northern sky with its unique set of 56 filters (R $\sim$ 60). Before, we observed 1 deg2 on the AEGIS field with an interim camera with all the J-PAS filters. With this data (miniJPAS), we aim at proving the scientific potential of J-PAS to identify and characterize the galaxy populations with the goal of performing galaxy evolution studies across cosmic time. Several SED-fitting codes are used to constrain the stellar population properties of a complete flux-limited sample (rSDSS <= 22.5 AB) of miniJPAS galaxies that extends up to z = 1. We find consistent results on the galaxy properties derived from the different codes, independently of the galaxy spectral-type or redshift. For galaxies with SNR>=10, we estimate that the J-PAS photometric system allows to derive stellar population properties with a precision that is equivalent to that obtained with spectroscopic surveys of similar SNR. By using the dust-corrected (u-r) colour-mass diagram, a powerful proxy to characterize galaxy populations, we find that the fraction of red and blue galaxies evolves with cosmic time, with red galaxies being $\sim$ 38% and $\sim$ 18% of the whole population at z = 0.1 and z = 0.5, respectively. At all redshifts, the more massive galaxies belong to the red sequence and these galaxies are typically older and more metal rich than their counterparts in the blue cloud. Our results confirm that with J-PAS data we will be able to analyze large samples of galaxies up to z $\sim$ 1, with galaxy stellar masses above of log(M$_*$/M$_{\odot}$) $\sim$ 8.9, 9.5, and 9.9 at z = 0.3, 0.5, and 0.7, respectively. The SFH of a complete sub-sample of galaxies selected at z $\sim$ 0.1 with log(M$_*$/M$_{\odot}$) > 8.3 constrain the cosmic evolution of the star formation rate density up to z $\sim$ 3 in good agreement with results from cosmological surveys. △ Less

Submitted 5 March, 2021; v1 submitted 25 February, 2021; originally announced February 2021.

Comments: 27 pages, 23 figures, 3 tables, accepted for publication in Astronomy & Astrophysics

Journal ref: A&A 649, A79 (2021)

Detection of supernova remnants in NGC 4030

Authors: Roberto Cid Fernandes, Maiara S. Carvalho, Sebastian F. Sanchez, Andre L. de Amorim, Daniel Ruschel-Dutra

Abstract: MUSE-based emission-line maps of the spiral galaxy NGC 4030 reveal the existence of unresolved sources with forbidden line emission enhanced with respect to those seen in its own HII regions. This study reports our efforts to detect and isolate these objects and identify their nature. Candidates are first detected as unresolved sources on an image of the second principal component of the Hb, [OIII… ▽ More MUSE-based emission-line maps of the spiral galaxy NGC 4030 reveal the existence of unresolved sources with forbidden line emission enhanced with respect to those seen in its own HII regions. This study reports our efforts to detect and isolate these objects and identify their nature. Candidates are first detected as unresolved sources on an image of the second principal component of the Hb, [OIII]5007, Ha, [NII]6584, [SII]6716, 6731 emission-line data cube, where they stand out clearly against both the dominant HII region population and the widespread diffuse emission. The intrinsic emission is then extracted accounting for the highly inhomogeneous emission-line "background" throughout the field of view. Collisional to recombination line ratios like [SII]/Ha, [NII]/Ha, and [OI]/Ha tend to increase when the background emission is corrected for. We find that many (but not all) sources detected with the principal component analysis have properties compatible with supernova remnants (SNRs). Applying a combined [SII]/Ha and [NII]/Ha classification criterion leads to a list of 59 sources with SNR-like emission lines. Many of them exhibit conspicuous spectral signatures of SNRs around 7300 Angs, and a stacking analysis shows that these features are also present, except weaker, in other cases. At nearly 30 Mpc, these are the most distant SNRs detected by optical means to date. We further report the serendipitous discovery of a luminous (M_V ~ -12.5), blue, and variable source, possibly associated with a supernova impostor. △ Less

Submitted 28 January, 2021; originally announced January 2021.

Comments: MNRAS, in press

J-PAS: Measuring emission lines with artificial neural networks

Authors: G. Martínez-Solaeche, R. M. González Delgado, R. García-Benito, A. de Amorim, E. Pérez, J. E. Rodríguez-Martín, L. A. Díaz-García, R. Cid Fernandes, C. López-Sanjuan, S. Bonoli, A. J. Cenarro, R. A. Dupke, A. Marín-Franch, J. Varela, H. Vázquez Ramió, L. R. Abramo, D. Cristóbal-Hornillo, M. Moles, J. Alcaniz, P. O. Baqui, N. Benitez, S. Carneiro, A. Cortesi, A. Ederoclite, V. Marra , et al. (5 additional authors not shown)

Abstract: Throughout this paper we present a new method to detect and measure emission lines in J-PAS up to $z = 0.35$. J-PAS will observe $8000$~deg$^2$ of the northern sky in the upcoming years with 56 photometric bands. The release of such amount of data brings us the opportunity to employ machine learning methods in order to overcome the difficulties associated with photometric data. We used Artificial… ▽ More Throughout this paper we present a new method to detect and measure emission lines in J-PAS up to $z = 0.35$. J-PAS will observe $8000$~deg$^2$ of the northern sky in the upcoming years with 56 photometric bands. The release of such amount of data brings us the opportunity to employ machine learning methods in order to overcome the difficulties associated with photometric data. We used Artificial Neural Networks (ANNs) trained and tested with synthetic J-PAS photometry from CALIFA, MaNGA, and SDSS spectra. We carry out two tasks: firstly, we cluster galaxies in two groups according to the values of the equivalent width (EW) of $Hα$, $Hβ$, $[NII]{λ6584}$, and $ [OIII]{λ5007}$ lines measured in the spectra. Then, we train an ANN to assign to each galaxy a group. We are able to classify them with the uncertainties typical of the photometric redshift measurable in J-PAS. Secondly, we utilize another ANN to determine the values of those EWs. Subsequently, we obtain the $[NII]/Hα$, $[OIII]/Hβ$, and \ion{O}{3}\ion{N}{2} ratios recovering the BPT diagram . We study the performance of the ANN in two training samples: one is only composed of synthetic J-PAS photo-spectra (J-spectra) from MaNGA and CALIFA (CALMa set) and the other one is composed of SDSS galaxies. We can reproduce properly the main sequence of star forming galaxies from the determination of the EWs. With the CALMa training set we reach a precision of 0.093 and 0.081 dex for the $[NII]/Hα$ and $[OIII]/Hβ$ ratios in the SDSS testing sample. Nevertheless, we find an underestimation of those ratios at high values in galaxies hosting an AGN. We also show the importance of the dataset used for both training and testing the model. ANNs are extremely useful to overcome the limitations previously expected concerning the detection and measurements of the emission lines in surveys like J-PAS. △ Less

Submitted 30 December, 2020; v1 submitted 10 August, 2020; originally announced August 2020.

Comments: 19 pages, 14 figures, Accepted to A&A

Journal ref: A&A 647, A158 (2021)

The miniJPAS survey: star-galaxy classification using machine learning

Authors: P. O. Baqui, V. Marra, L. Casarini, R. Angulo, L. A. Díaz-García, C. Hernández-Monteagudo, P. A. A. Lopes, C. López-Sanjuan, D. Muniesa, V. M. Placco, M. Quartin, C. Queiroz, D. Sobral, E. Solano, E. Tempel, J. Varela, J. M. Vílchez, R. Abramo, J. Alcaniz, N. Benitez, S. Bonoli, S. Carneiro, A. J. Cenarro, D. Cristóbal-Hornillos, A. L. de Amorim , et al. (9 additional authors not shown)

Abstract: Future astrophysical surveys such as J-PAS will produce very large datasets, which will require the deployment of accurate and efficient Machine Learning (ML) methods. In this work, we analyze the miniJPAS survey, which observed about 1 deg2 of the AEGIS field with 56 narrow-band filters and 4 ugri broad-band filters. We discuss the classification of miniJPAS sources into extended (galaxies) and p… ▽ More Future astrophysical surveys such as J-PAS will produce very large datasets, which will require the deployment of accurate and efficient Machine Learning (ML) methods. In this work, we analyze the miniJPAS survey, which observed about 1 deg2 of the AEGIS field with 56 narrow-band filters and 4 ugri broad-band filters. We discuss the classification of miniJPAS sources into extended (galaxies) and point-like (e.g. stars) objects, a necessary step for the subsequent scientific analyses. We aim at developing an ML classifier that is complementary to traditional tools based on explicit modeling. In order to train and test our classifiers, we crossmatched the miniJPAS dataset with SDSS and HSC-SSP data. We trained and tested 6 different ML algorithms on the two crossmatched catalogs. As input for the ML algorithms we use the magnitudes from the 60 filters together with their errors, with and without the morphological parameters. We also use the mean PSF in the r detection band for each pointing. We find that the RF and ERT algorithms perform best in all scenarios. When analyzing the full magnitude range of 15<r<23.5 we find AUC=0.957 with RF when using only photometric information, and AUC=0.986 with ERT when using photometric and morphological information. Regarding feature importance, when using morphological parameters, FWHM is the most important feature. When using photometric information only, we observe that broad bands are not necessarily more important than narrow bands, and errors are as important as the measurements. ML algorithms can compete with traditional star/galaxy classifiers, outperforming the latter at fainter magnitudes (r>21). We use our best classifiers, with and without morphology, in order to produce a value added catalog available at https://j-pas.org/datareleases . △ Less

Submitted 12 November, 2020; v1 submitted 15 July, 2020; originally announced July 2020.

Comments: 19 pages, 17 figures. New Appendices E & F and improved discussion. VAC available at https://j-pas.org/datareleases . Trained models available at https://github.com/J-PAS-collaboration/StarGalClass-MachineLearning . Abstract abridged to meet arXiv requirements. Version accepted for publication in A&A

Journal ref: A&A 645, A87 (2021)

Less than the sum of its parts: the dust-corrected H$α$ luminosity of star-forming galaxies explored at different spatial resolutions with MaNGA and MUSE

Authors: N. Vale Asari, V. Wild, A. L. de Amorim, A. Werle, Y. Zheng, R. Kennicutt, B. D. Johnson, M. Galametz, E. W. Pellegrini, R. S. Klessen, S. Reissl, S. C. O. Glover, D. Rahner

Abstract: The H$α$ and H$β$ emission line luminosities measured in a single integrated spectrum are affected in non-trivial ways by point-to-point variations in dust attenuation in a galaxy. This work investigates the impact of this variation when estimating global H$α$ luminosities corrected for the presence of dust by a global Balmer decrement. Analytical arguments show that the dust-corrected H$α$ lumino… ▽ More The H$α$ and H$β$ emission line luminosities measured in a single integrated spectrum are affected in non-trivial ways by point-to-point variations in dust attenuation in a galaxy. This work investigates the impact of this variation when estimating global H$α$ luminosities corrected for the presence of dust by a global Balmer decrement. Analytical arguments show that the dust-corrected H$α$ luminosity is always underestimated when using the global H$α$/H$β$ flux ratio to correct for dust attenuation. We measure this effect on 156 face-on star-forming galaxies from the Mapping Nearby Galaxies at APO (MaNGA) survey. At 1-2 kpc spatial resolution, the effect is small but systematic, with the integrated dust-corrected H$α$ luminosity underestimated by $2$-$4$ per cent (and typically not more than by $10$ per cent), and depends on the specific star formation rate of the galaxy. Given the spatial resolution of MaNGA, these are lower limits for the effect. From Multi Unit Spectroscopic Explorer (MUSE) observations of NGC 628 with a resolution of 36 pc we find the discrepancy between the globally and the point-by-point dust-corrected H$α$ luminosity to be $14 \pm 1$ per cent, which may still underestimate the true effect. We use toy models and simulations to show that the true difference depends strongly on the spatial variance of the H$α$/H$β$ flux ratio, and on the slope of the relation between H$α$ luminosity and dust attenuation within a galaxy. Larger samples of higher spatial resolution observations are required to quantify the dependence of this effect as a function of galaxy properties. △ Less

Submitted 9 September, 2020; v1 submitted 10 July, 2020; originally announced July 2020.

Comments: MNRAS accepted

The miniJPAS survey: a preview of the Universe in 56 colours

Authors: S. Bonoli, A. Marín-Franch, J. Varela, H. Vázquez Ramió, L. R. Abramo, A. J. Cenarro, R. A. Dupke, J. M. Vílchez, D. Cristóbal-Hornillos, R. M. González Delgado, C. Hernández-Monteagudo, C. López-Sanjuan, D. J. Muniesa, T. Civera, A. Ederoclite, A. Hernán-Caballero, V. Marra, P. O. Baqui, A. Cortesi, E. S. Cypriano, S. Daflon, A. L. de Amorim, L. A. Díaz-García, J. M. Diego, G. Martínez-Solaeche , et al. (144 additional authors not shown)

Abstract: The Javalambre-Physics of the Accelerating Universe Astrophysical Survey (J-PAS) will soon start to scan thousands of square degrees of the northern extragalactic sky with a unique set of $56$ optical filters from a dedicated $2.55$m telescope, JST, at the Javalambre Astrophysical Observatory. Before the arrival of the final instrument (a 1.2 Gpixels, 4.2deg$^2$ field-of-view camera), the JST was… ▽ More The Javalambre-Physics of the Accelerating Universe Astrophysical Survey (J-PAS) will soon start to scan thousands of square degrees of the northern extragalactic sky with a unique set of $56$ optical filters from a dedicated $2.55$m telescope, JST, at the Javalambre Astrophysical Observatory. Before the arrival of the final instrument (a 1.2 Gpixels, 4.2deg$^2$ field-of-view camera), the JST was equipped with an interim camera (JPAS-Pathfinder), composed of one CCD with a 0.3deg$^2$ field-of-view and resolution of 0.23 arcsec pixel$^{-1}$. To demonstrate the scientific potential of J-PAS, with the JPAS-Pathfinder camera we carried out a survey on the AEGIS field (along the Extended Groth Strip), dubbed miniJPAS. We observed a total of $\sim 1$ deg$^2$, with the $56$ J-PAS filters, which include $54$ narrow band (NB, $\rm{FWHM} \sim 145$Angstrom) and two broader filters extending to the UV and the near-infrared, complemented by the $u,g,r,i$ SDSS broad band (BB) filters. In this paper we present the miniJPAS data set, the details of the catalogues and data access, and illustrate the scientific potential of our multi-band data. The data surpass the target depths originally planned for J-PAS, reaching $\rm{mag}_{\rm {AB}}$ between $\sim 22$ and $23.5$ for the NB filters and up to $24$ for the BB filters ($5σ$ in a $3$~arcsec aperture). The miniJPAS primary catalogue contains more than $64,000$ sources extracted in the $r$ detection band with forced photometry in all other bands. We estimate the catalogue to be complete up to $r=23.6$ for point-like sources and up to $r=22.7$ for extended sources. Photometric redshifts reach subpercent precision for all sources up to $r=22.5$, and a precision of $\sim 0.3$% for about half of the sample. (Abridged) △ Less

Submitted 9 July, 2020; v1 submitted 3 July, 2020; originally announced July 2020.

Comments: The miniJPAS data and associated value added catalogues are publicly accessible via this url: http://archive.cefca.es/catalogues/minijpas-pdr201912

Journal ref: A&A 653, A31 (2021)

Clues on the history of early-type galaxies from SDSS spectra and GALEX photometry

Authors: Ariel Werle, Roberto Cid Fernandes, Natalia Vale Asari, Paula R. T. Coelho, Gustavo Bruzual, Stephane Charlot, Reinaldo R. de Carvalho, Fábio R. Herpich, Clauda Mendes de Oliveira, Laerte Sodré Jr., Daniel Ruschel Dutra, André de Amorim, Vitor M. Sampaio

Abstract: Stellar population studies of early-type galaxies (ETGs) based on their optical stellar continuum suggest that these are quiescent systems. However, emission lines and ultraviolet photometry reveal a diverse population. We use a new version of the STARLIGHT spectral synthesis code and state-of-the-art stellar population models to simultaneously fit SDSS spectra and GALEX photometry for a sample of… ▽ More Stellar population studies of early-type galaxies (ETGs) based on their optical stellar continuum suggest that these are quiescent systems. However, emission lines and ultraviolet photometry reveal a diverse population. We use a new version of the STARLIGHT spectral synthesis code and state-of-the-art stellar population models to simultaneously fit SDSS spectra and GALEX photometry for a sample of 3453 galaxies at $z < 0.1$ with $NUV-r > 5$ that are classified as elliptical by Galaxy Zoo. We reproduce $FUV$ magnitudes for 80 per cent of UV upturn galaxies selected using criteria from the literature, suggesting that additional stellar population ingredients such as binaries and extreme horizontal branch stars may have a limited contribution to the UV upturn. The addition of ultraviolet data leads to a broadening of the distributions of mean stellar ages, metallicities and attenuation. Stellar populations younger than $1\,$Gyr are required to reproduce the ultraviolet emission in 17 per cent of our sample. These systems represent 43 per cent of the sample at $5<NUV-r<5.5$ and span the same stellar mass range as other ETGs in our sample. ETGs with young stellar components have larger $Hα$ equivalent widths ($W_{Hα}$) and larger dust attenuation. Emission line ratios and $W_{Hα}$ indicate that the ionising source in these systems is a mixture of young and old stellar populations. Their young stellar populations are metal-poor, especially for high-mass galaxies, indicating recent star formation associated with rejuvenation events triggered by external processes, such as minor mergers. △ Less

Submitted 30 July, 2020; v1 submitted 2 July, 2020; originally announced July 2020.

Comments: Accepted for publication in MNRAS

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.

Comments: Coq code can be found at https://github.com/FLAFOL/flafol-coq

SIGNALS: I. Survey Description

Authors: L. Rousseau-Nepton, R. P. Martin, C. Robert, L. Drissen, P. Amram, S. Prunet, T. Martin, I. Moumen, A. Adamo, A. Alarie, P. Barmby, A. Boselli, F. Bresolin, M. Bureau, L. Chemin, R. C. Fernandes, F. Combes, C. Crowder, L. Della Bruna, F. Egusa, B. Epinat, V. F. Ksoll, M. Girard, V. Gómez Llanos, D. Gouliermis , et al. (38 additional authors not shown)

Abstract: SIGNALS, the Star formation, Ionized Gas, and Nebular Abundances Legacy Survey, is a large observing program designed to investigate massive star formation and HII regions in a sample of local extended galaxies. The program will use the imaging Fourier transform spectrograph SITELLE at the Canada-France-Hawaii Telescope. Over 355 hours (54.7 nights) have been allocated beginning in fall 2018 for e… ▽ More SIGNALS, the Star formation, Ionized Gas, and Nebular Abundances Legacy Survey, is a large observing program designed to investigate massive star formation and HII regions in a sample of local extended galaxies. The program will use the imaging Fourier transform spectrograph SITELLE at the Canada-France-Hawaii Telescope. Over 355 hours (54.7 nights) have been allocated beginning in fall 2018 for eight consecutive semesters. Once completed, SIGNALS will provide a statistically reliable laboratory to investigate massive star formation, including over 50 000 resolved HII regions : the largest, most complete, and homogeneous database of spectroscopically and spatially resolved extragalactic HII regions ever assembled. For each field observed, three datacubes covering the spectral bands of the filters SN1 (363 -386 nm), SN2 (482 - 513 nm), and SN3 (647 - 685 nm) are gathered. The spectral resolution selected for each spectral band is 1000, 1000, and 5000, respectively. As defined, the project sample will facilitate the study of small-scale nebular physics and many other phenomena linked to star formation at a mean spatial resolution of 20 pc. This survey also has considerable legacy value for additional topics including planetary nebulae, diffuse ionized gas, andsupernova remnants. The purpose of this paper is to present a general outlook of the survey, notably the observing strategy, galaxy sample, and science requirements. △ Less

Submitted 23 August, 2019; originally announced August 2019.

Comments: 19 pages, 14 figures, submitted to MNRAS

Diffuse ionized gas and its effects on nebular metallicity estimates of star-forming galaxies

Authors: N. Vale Asari, G. S. Couto, R. Cid Fernandes, G. Stasińska, A. L. de Amorim, D. Ruschel-Dutra, A. Werle, T. Z. Florido

Abstract: We investigate the impact of the diffuse ionized gas (DIG) on abundance determinations in star-forming (SF) galaxies. The DIG is characterised using the H$α$ equivalent width ($W_{\text{H}α}$). From a set of 1,409 SF galaxies from the Mapping Nearby Galaxies at APO (MaNGA) survey, we calculate the fractional contribution of the DIG to several emission lines using high-$S/N$ data from SF spaxels (i… ▽ More We investigate the impact of the diffuse ionized gas (DIG) on abundance determinations in star-forming (SF) galaxies. The DIG is characterised using the H$α$ equivalent width ($W_{\text{H}α}$). From a set of 1,409 SF galaxies from the Mapping Nearby Galaxies at APO (MaNGA) survey, we calculate the fractional contribution of the DIG to several emission lines using high-$S/N$ data from SF spaxels (instead of using noisy emission-lines in DIG-dominated spaxels). Our method is applicable to spectra with observed $W_{\text{H}α} \gtrsim 10$ angstroms (which are not dominated by DIG emission). Since the DIG contribution depends on galactocentric distance, we provide DIG-correction formulae for both entire galaxies and single aperture spectra. Applying those to a sample of $\,> 90,000$ SF galaxies from the Sloan Digital Sky Survey, we find the following. (1) The effect of the DIG on strong-line abundances depends on the index used. It is negligible for the ([O III]/H$β$)/([N II]/H$α$) index, but reaches $\sim 0.1$ dex at the high-metallicity end for [N II]/H$α$. (2) This result is based on the $\sim$kpc MaNGA resolution, so the real effect of the DIG is likely greater. (3) We revisit the mass-metallicity-star formation rate (SFR) relation by correcting for the DIG contribution in both abundances and SFR. The effect of DIG removal is more prominent at higher stellar masses. Using the [N II]/H$α$ index, O/H increases with SFR at high stellar mass, contrary to previous claims. △ Less

Submitted 2 September, 2019; v1 submitted 19 July, 2019; originally announced July 2019.

Comments: Accepted for publication in MNRAS

Spatially resolved mass-to-light from the CALIFA survey. Mass-to-light ratio vs. color relations

Authors: R. García-Benito, R. M. González Delgado, E. Pérez, R. Cid Fernandes, S. F. Sánchez, A. L. de Amorim

Abstract: We investigated the mass-to-light versus color relations (MLCRs) derived from the spatially resolved star formation history of a sample of 452 galaxies observed with integral field spectroscopy in the CALIFA survey. We derived the stellar mass ($M_\star$) and the stellar mass surface density from the combination of full spectral fitting (using different sets of stellar population models) with obse… ▽ More We investigated the mass-to-light versus color relations (MLCRs) derived from the spatially resolved star formation history of a sample of 452 galaxies observed with integral field spectroscopy in the CALIFA survey. We derived the stellar mass ($M_\star$) and the stellar mass surface density from the combination of full spectral fitting (using different sets of stellar population models) with observed and synthetic colors in optical broad bands. This method allows obtaining the radial structure of the mass-to-light ratio ($M/L$) at several wavelengths and studying the spatially resolved MLCRs. Our sample covers a wide range of Hubble types from Sc to E, with stellar masses ranging from $M_\star \sim 10^{8.4}$ to $10^{12}$ M$_\odot$. The scatter in the MLCRs was studied as a function of morphology, stellar extinction, and emission line contribution to the colors. The effects of the initial mass function (IMF) and stellar population models in the MLCRs were also explored. Our main results are that (a) the $M/L$ ratio has a negative radial gradient that is steeper within the central 1 half-light-radius (HLR). It is steeper in Sb-Sbc than in early-type galaxies. (b) The MLCRs between $M/L$ and optical colors were derived with a scatter of $\sim$ 0.1 dex. Extinction and emission line contributions do not affect the scatter of these relations. Morphology does not produce a significant effect, except if the general relation is used for galaxies redder than $(u-i) > 4$ or bluer than $(u-i) < 0$. (c) The IMF has a large effect on MLCRs, as expected. The change from a Chabrier to a Salpeter IMF produces a median shift of $\sim$ \oimf\ dex when mass loss from stellar evolution is also taken into account. (d) These MLCRs are in agreement with previous results, in particular for relations with $g$ and $r$ bands and the $B$ and $V$ Johnson systems. FITS tables available at http://pycasso.iaa.es/ML △ Less

Submitted 20 November, 2018; originally announced November 2018.

Comments: 13 pages, 10 figures, 12 tables, accepted for publication in Astronomy & Astrophysics. Abridged abstract. All tables are available in electronic format at http://pycasso.iaa.es/ML

Journal ref: A&A 621, A120 (2019)

Probabilistic Relational Reasoning via Metrics

Authors: Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata

Abstract: The Fuzz programming language [Reed and Pierce, 2010] uses an elegant linear type system combined with a monad-like type to express and reason about probabilistic sensitivity properties, most notably $ε$-differential privacy. We show how to extend Fuzz to capture more general relational properties of probabilistic programs, with approximate, or $(ε, δ)$-differential privacy serving as a leading ex… ▽ More The Fuzz programming language [Reed and Pierce, 2010] uses an elegant linear type system combined with a monad-like type to express and reason about probabilistic sensitivity properties, most notably $ε$-differential privacy. We show how to extend Fuzz to capture more general relational properties of probabilistic programs, with approximate, or $(ε, δ)$-differential privacy serving as a leading example. Our technical contributions are threefold. First, we introduce the categorical notion of comonadic lifting of a monad to model composition properties of probabilistic divergences. Then, we show how to express relational properties in terms of sensitivity properties via an adjunction we call the path construction. Finally, we instantiate our semantics to model the terminating fragment of Fuzz extended with types carrying information about other divergences between distributions. △ Less

Submitted 18 April, 2019; v1 submitted 13 July, 2018; originally announced July 2018.

When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise

Authors: Carmine Abate, Arthur Azevedo de Amorim, Roberto Blanco, Ana Nora Evans, Guglielmo Fachini, Catalin Hritcu, Théo Laurent, Benjamin C. Pierce, Marco Stronati, Jérémy Thibault, Andrew Tolmach

Abstract: We propose a new formal criterion for evaluating secure compilation schemes for unsafe languages, expressing end-to-end security guarantees for software components that may become compromised after encountering undefined behavior---for example, by accessing an array out of bounds. Our criterion is the first to model dynamic compromise in a system of mutually distrustful components with clearly s… ▽ More We propose a new formal criterion for evaluating secure compilation schemes for unsafe languages, expressing end-to-end security guarantees for software components that may become compromised after encountering undefined behavior---for example, by accessing an array out of bounds. Our criterion is the first to model dynamic compromise in a system of mutually distrustful components with clearly specified privileges. It articulates how each component should be protected from all the others---in particular, from components that have encountered undefined behavior and become compromised. Each component receives secure compilation guarantees---in particular, its internal invariants are protected from compromised components---up to the point when this component itself becomes compromised, after which we assume an attacker can take complete control and use this component's privileges to attack other components. More precisely, a secure compilation chain must ensure that a dynamically compromised component cannot break the safety properties of the system at the target level any more than an arbitrary attacker-controlled component (with the same interface and privileges, but without undefined behaviors) already could at the source level. To illustrate the model, we construct a secure compilation chain for a small unsafe language with buffers, procedures, and components, targeting a simple abstract machine with built-in compartmentalization. We give a machine-checked proof in Coq that this compiler satisfies our secure compilation criterion. Finally, we show that the protection guarantees offered by the compartmentalized abstract machine can be achieved at the machine-code level using either software fault isolation or a tag-based reference monitor. △ Less

Submitted 29 November, 2019; v1 submitted 2 February, 2018; originally announced February 2018.

Comments: CCS paper with significant improvement of the proofs, first step towards a journal version

Diffuse ionized gas in galaxies across the Hubble sequence at the CALIFA resolution

Authors: E. A. D. Lacerda, R. Cid Fernandes, G. S. Couto, G. Stasinska, R. Garcia-Benito, N. Vale Asari, E. Perez, R. M. Gonzalez Delgado, S. F. Sanchez, A. L. de Amorim

Abstract: We use spatially resolved spectroscopy from the Calar Alto Legacy Field Area (CALIFA) survey to study the nature of the line emitting gas in galaxies of different Hubble types, focusing on the separation of star-forming (SF) regions from those better characterized as diffuse ionized gas (DIG). The diagnosis is carried out in terms of the equivalent width of ${\rm H}α$ ($W_{{\rm H}α}$). Three nebul… ▽ More We use spatially resolved spectroscopy from the Calar Alto Legacy Field Area (CALIFA) survey to study the nature of the line emitting gas in galaxies of different Hubble types, focusing on the separation of star-forming (SF) regions from those better characterized as diffuse ionized gas (DIG). The diagnosis is carried out in terms of the equivalent width of ${\rm H}α$ ($W_{{\rm H}α}$). Three nebular regimes are identified. Regions where $W_{{\rm H}α} < 3\ Å$ define what we call the hDIG, the component of the DIG where photoionization is dominated by hot, low-mass, evolved stars. Regions where $W_{{\rm H}α} > 14\ Å$ trace SF complexes. $W_{{\rm H}α}$ values in the intermediate 3--14 $Å$ range reflect a mixed regime (mDIG) where more than one process contributes. This three-tier scheme is inspired both by theoretical and empirical considerations. Its application to CALIFA galaxies of different types and inclinations leads to the following results: $\textit{(i)}$ the hDIG component is prevalent throughout ellipticals and S0's as well as in bulges, and explains the strongly bimodal distribution of $W_{{\rm H}α}$ both among and within galaxies. $\textit{(ii)}$ Early-type spirals have some hDIG in their discs, but this component becomes progressively less relevant for later Hubble types. $\textit{(iii)}$ hDIG emission is also present above and below galactic discs, as seen in several edge-on spirals in our sample. $\textit{(iv)}$ The SF/mDIG proportion grows steadily from early- to late-type spirals, and from inner to outer radii. $\textit{(v)}$ Besides circumventing basic inconsistencies in conventional DIG/SF separation criteria based on the ${\rm H}α$ surface brightness, our $W_{{\rm H}α}$-based method produces results in agreement with a classical excitation diagram analysis. △ Less

Submitted 20 December, 2017; v1 submitted 21 November, 2017; originally announced November 2017.

Comments: Accepted for publication in MNRAS, 14 pages, 9 Figures

Formally Secure Compilation of Unsafe Low-Level Components (Extended Abstract)

Authors: Guglielmo Fachini, Catalin Hritcu, Marco Stronati, Ana Nora Evans, Théo Laurent, Arthur Azevedo de Amorim, Benjamin C. Pierce, Andrew Tolmach

Abstract: We propose a new formal criterion for secure compilation, providing strong security guarantees for components written in unsafe, low-level languages with C-style undefined behavior. Our criterion goes beyond recent proposals, which protect the trace properties of a single component against an adversarial context, to model dynamic compromise in a system of mutually distrustful components. Each comp… ▽ More We propose a new formal criterion for secure compilation, providing strong security guarantees for components written in unsafe, low-level languages with C-style undefined behavior. Our criterion goes beyond recent proposals, which protect the trace properties of a single component against an adversarial context, to model dynamic compromise in a system of mutually distrustful components. Each component is protected from all the others until it receives an input that triggers an undefined behavior, causing it to become compromised and attack the remaining uncompromised components. To illustrate this model, we demonstrate a secure compilation chain for an unsafe language with buffers, procedures, and components, compiled to a simple RISC abstract machine with built-in compartmentalization. The protection guarantees offered by this abstract machine can be achieved at the machine-code level using either software fault isolation or tag-based reference monitoring. We are working on machine-checked proofs showing that this compiler satisfies our secure compilation criterion. △ Less

Submitted 31 October, 2017; v1 submitted 19 October, 2017; originally announced October 2017.

Comments: PriSC'18 submission, updated to fix a few things

The spatially resolved star formation history of CALIFA galaxies: Cosmic time scales

Authors: R. García-Benito, R. M. González Delgado, E. Pérez, R. Cid Fernandes, C. Cortijo-Ferrero, R. López Fernández, A. L. de Amorim, E. A. D. Lacerda, N. Vale Asari, S. F. Sánchez

Abstract: This paper presents the mass assembly time scales of nearby galaxies observed by CALIFA at the 3.5m telescope in Calar Alto. We apply the fossil record method of the stellar populations to the complete sample of the 3rd CALIFA data release, with a total of 661 galaxies, covering stellar masses from 10$^{8.4}$ to 10$^{12}$ M$_{\odot}$ and a wide range of Hubble types. We apply spectral synthesis te… ▽ More This paper presents the mass assembly time scales of nearby galaxies observed by CALIFA at the 3.5m telescope in Calar Alto. We apply the fossil record method of the stellar populations to the complete sample of the 3rd CALIFA data release, with a total of 661 galaxies, covering stellar masses from 10$^{8.4}$ to 10$^{12}$ M$_{\odot}$ and a wide range of Hubble types. We apply spectral synthesis techniques to the datacubes and process the results to produce the mass growth time scales and mass weighted ages, from which we obtain temporal and spatially resolved information in seven bins of galaxy morphology and six bins of stellar mass (M$_{\star}$) and stellar mass surface density ($Σ_{\star}$). We use three different tracers of the spatially resolved star formation history (mass assembly curves, ratio of half mass to half light radii, and mass-weighted age gradients) to test if galaxies grow inside-out, and its dependence with galaxy stellar mass, $Σ_{\star}$, and morphology. Our main results are as follows: (a) The innermost regions of galaxies assemble their mass at an earlier time than regions located in the outer parts; this happens at any given M$_{\star}$, $Σ_{\star}$, or Hubble type, including the lowest mass systems. (b) Galaxies present a significant diversity in their characteristic formation epochs for lower-mass systems. This diversity shows a strong dependence of the mass assembly time scales on $Σ_{\star}$ and Hubble type in the lower-mass range (10$^{8.4}$ to 10$^{10.4}$), but a very mild dependence in higher-mass bins. (c) All galaxies show negative $\langle$log age$\rangle_{M}$ gradients in the inner 1 HLR. The profile flattens with increasing values of $Σ_{\star}$. There is no significant dependence on M$_{\star}$ within a particular $Σ_{\star}$ bin, except for the lowest bin, where the gradients becomes steeper. △ Less

Submitted 1 September, 2017; originally announced September 2017.

Comments: 15 pages, 13 figures, 3 tables, accepted for publication in Astronomy & Astrophysics. *Abridged abstract*

Journal ref: A&A 608, A27 (2017)

The spatially resolved star formation history of mergers: A comparative study of the LIRGs IC1623, NGC6090, NGC2623, and Mice

Authors: C. Cortijo-Ferrero, R. M. González Delgado, E. Pérez, R. Cid Fernandes, R. García-Benito, P. Di Matteo, S. F. Sánchez, A. L. de Amorim, E. A. D. Lacerda, R. López Fernández, C. Tadhunter

Abstract: This paper presents the spatially resolved star formation history (2D-SFH) of a small sample of four local mergers: the early-stage mergers IC1623, NGC6090, and the Mice, and the more advanced merger NGC2623, by analyzing IFS data from the CALIFA survey and PMAS in LArr mode. Full spectral fitting techniques are applied to the datacubes to obtain the spatially resolved mass growth histories, the t… ▽ More This paper presents the spatially resolved star formation history (2D-SFH) of a small sample of four local mergers: the early-stage mergers IC1623, NGC6090, and the Mice, and the more advanced merger NGC2623, by analyzing IFS data from the CALIFA survey and PMAS in LArr mode. Full spectral fitting techniques are applied to the datacubes to obtain the spatially resolved mass growth histories, the time evolution of the star formation rate intensity ($Σ_{SFR}$), and the local specific star formation rate, over three different timescales (30 Myr, 300 Myr, and 1 Gyr). The results are compared with non-interacting Sbc--Sc galaxies, to quantify if there is an enhancement of the star formation and to trace its time scale and spatial extent. Our results for the three LIRGs (IC1623W, NGC6090, and NGC2623) show that a major phase of star formation is occurring in time scales of 10$^{7}$ yr to few 10$^{8}$ yr, with global SFR enhancements of $\sim$2--6 with respect to main-sequence star forming (MSSF) galaxies. In the two early-stage mergers IC1623W and NGC6090, which are between first pericenter passage and coalescence, the most remarkable increase of the SFR with respect to non-interacting spirals occurred in the last 30 Myr, and it is spatially extended, with enhancements of factors 2--7 both in the centres ($r <$ 0.5 half light radius, HLR), and in the disks ($r >$ 1 HLR). In the more advanced merger NGC 2623 an extended phase of star formation occurred on a longer time-scale of $\sim$1 Gyr, with a SFR enhancement of a factor $\sim$2--3 larger than the one in Sbc--Sc MSSF galaxies over the same period, probably relic of the first pericenter passage epoch. A SFR enhancement in the last 30 Myr is also present, but only in NGC2623 centre, by a factor 3. In general, the spatially resolved SFHs of the LIRG-mergers are consistent with the predictions from high spatial resolution simulations. △ Less

Submitted 17 July, 2017; originally announced July 2017.

Comments: 17 pages, 7 figures, 2 tables, accepted for publication in Astronomy & Astrophysics, abstract abridged for arXiv submission

Journal ref: A&A 607, A70 (2017)

The PyCASSO database: Spatially resolved stellar population properties for CALIFA galaxies

Authors: A. L. de Amorim, R. García-Benito, R. Cid Fernandes, C. Cortijo-Ferrero, R. M. González Delgado, E. A. D. Lacerda, R. López Fernández, E. Pérez, N. Vale Asari

Abstract: The Calar Alto Legacy Integral Field Area (CALIFA) survey, a pioneer in integral field spectroscopy legacy projects, has fostered many studies exploring the information encoded on the spatially resolved data on gaseous and stellar features in the optical range of galaxies. We describe a value-added catalogue of stellar population properties for CALIFA galaxies analysed with the spectral synthesis… ▽ More The Calar Alto Legacy Integral Field Area (CALIFA) survey, a pioneer in integral field spectroscopy legacy projects, has fostered many studies exploring the information encoded on the spatially resolved data on gaseous and stellar features in the optical range of galaxies. We describe a value-added catalogue of stellar population properties for CALIFA galaxies analysed with the spectral synthesis code STARLIGHT and processed with the PyCASSO platform. Our public data base (http://pycasso.ufsc.br/, mirror at http://pycasso.iaa.es/) comprises 445 galaxies from the CALIFA Data Release 3 with COMBO data. The catalogue provides maps for the stellar mass surface density, mean stellar ages and metallicities, stellar dust attenuation, star formation rates, and kinematics. Example applications both for individual galaxies and for statistical studies are presented to illustrate the power of this data set. We revisit and update a few of our own results on mass density radial profiles and on the local mass-metallicity relation. We also show how to employ the catalogue for new investigations, and show a pseudo Schmidt-Kennicutt relation entirely made with information extracted from the stellar continuum. Combinations to other databases are also illustrated. Among other results, we find a very good agreement between star formation rate surface densities derived from the stellar continuum and the $\mathrm{H}α$ emission. This public catalogue joins the scientific community's effort towards transparency and reproducibility, and will be useful for researchers focusing on (or complementing their studies with) stellar properties of CALIFA galaxies. △ Less

Submitted 17 July, 2017; originally announced July 2017.

Comments: 28 pages, 22 figures, accepted by MNRAS, access database at http://www.pycasso.ufsc.br/ and http://www.pycasso.iaa.es/

The spatially-resolved star formation histories of CALIFA galaxies: Implications for galaxy formation

Authors: R. M. González Delgado, E. Pérez, R. Cid Fernandes, R. García-Benito, R. López Fernández, N. Vale Asari, C. Cortijo-Ferrero, A. L. de Amorim, E. A. D. Lacerda, S. F. Sánchez, M. D. Lehnert, C. J. Walcher

Abstract: This paper presents the spatially resolved star formation history (SFH) of nearby galaxies with the aim of furthering our understanding of the different processes involved in the formation and evolution of galaxies. To this end, we apply the fossil record method of stellar population synthesis to a rich and diverse data set of 436 galaxies observed with integral field spectroscopy in the CALIFA su… ▽ More This paper presents the spatially resolved star formation history (SFH) of nearby galaxies with the aim of furthering our understanding of the different processes involved in the formation and evolution of galaxies. To this end, we apply the fossil record method of stellar population synthesis to a rich and diverse data set of 436 galaxies observed with integral field spectroscopy in the CALIFA survey. The sample covers a wide range of Hubble types, with stellar masses ranging from $M_\star \sim 10^9$ to $7 \times 10^{11} M_\odot$. Spectral synthesis techniques are applied to the datacubes to retrieve the spatially resolved time evolution of the star formation rate (SFR), its intensity ($Σ_{\rm SFR}$), and other descriptors of the 2D-SFH in seven bins of galaxy morphology (E, S0, Sa, Sb, Sbc, Sc, and Sd), and five bins of stellar mass. Our main results are: a) Galaxies form very fast independently of their current stellar mass, with the peak of star formation at high redshift ($z > 2$). Subsequent star formation is driven by $M_\star$ and morphology, with less massive and later type spirals showing more prolonged periods of star formation. b) At any epoch in the past the SFR is proportional to $M_\star$, with most massive galaxies having the highest absolute (but lowest specific) SFRs. c) While nowadays $Σ_{\rm SFR}$ is similar for all spirals, and significantly lower in early type galaxies (ETG), in the past $Σ_{\rm SFR}$ scales well with morphology. The central regions of today's ETGs are where $Σ_{\rm SFR}$ reached the highest values ($> 10^3 \,M_\odot\,$Gyr$^{-1}\,$pc$^{-2}$), similar to those measured in high redshift star forming galaxies. d) The evolution of $Σ_{\rm SFR}$ in Sbc systems matches that of models for Milky-Way-like galaxies, suggesting that the formation of a thick disk may be a common phase in spirals at early epochs. △ Less

Submitted 19 June, 2017; originally announced June 2017.

Comments: 21 pages, 11 figures, 1 table, accepted for publication in Astronomy & Astrophysics, abstract abridged for arXiv submission

Journal ref: A&A 607, A128 (2017)

The spatially resolved stellar population and ionized gas properties in the merger LIRG NGC 2623

Authors: C. Cortijo-Ferrero, R. M. González Delgado, E. Pérez, S. F. Sánchez, R. Cid Fernandes, A. L. de Amorim, P. Di Matteo, R. García-Benito, E. A. D. Lacerda, R. López Fernández, C. Tadhunter, M. Villar-Martín, M. M. Roth

Abstract: We report on a detailed study of the stellar populations and ionized gas properties in the merger LIRG NGC 2623, analysing optical Integral Field Spectroscopy from the CALIFA survey and PMAS LArr, multiwavelength HST imaging, and OSIRIS narrow band H$α$ and [NII]$λ$6584 imaging. The spectra were processed with the STARLIGHT full spectral fitting code, and the results compared with those for two ea… ▽ More We report on a detailed study of the stellar populations and ionized gas properties in the merger LIRG NGC 2623, analysing optical Integral Field Spectroscopy from the CALIFA survey and PMAS LArr, multiwavelength HST imaging, and OSIRIS narrow band H$α$ and [NII]$λ$6584 imaging. The spectra were processed with the STARLIGHT full spectral fitting code, and the results compared with those for two early-stage merger LIRGs (IC 1623 W and NGC 6090), together with CALIFA Sbc/Sc galaxies. We find that NGC 2623 went through two periods of increased star formation (SF), a first and widespread episode, traced by intermediate-age stellar populations ISP (140 Myr-1.4 Gyr), and a second one, traced by young stellar populations YSP ($<$140 Myr), which is concentrated in the central regions ($<$1.4 kpc). Our results are in agreement with the epochs of the first peri-center passage ($\sim$200 Myr ago) and coalescence ($<$100 Myr ago) predicted by dynamical models, and with high resolution merger simulations in the literature, consistent with NGC 2623 representing an evolved version of the early-stage mergers. Most ionized gas is concentrated within $<$2.8 kpc, where LINER-like ionization and high velocity dispersion ($\sim$220 km/s) are found, consistent with the previously reported outflow. As revealed by the highest resolution OSIRIS and HST data, a collection of HII regions is also present in the plane of the galaxy, which explains the mixture of ionization mechanisms in this system. It is unlikely that the outflow in NGC 2623 will escape from the galaxy, given the low SFR intensity ($\sim$0.5 M$_{\odot}$yr$^{-1}$kpc$^{-2}$), the fact that the outflow rate is 3 times lower than the current SFR, and the escape velocity in the central areas higher than the outflow velocity. △ Less

Submitted 6 June, 2017; originally announced June 2017.

Comments: 22 pages, 24 figures, accepted for publication in A&A

Journal ref: A&A 606, A95 (2017)

The Meaning of Memory Safety

Authors: Arthur Azevedo de Amorim, Catalin Hritcu, Benjamin C. Pierce

Abstract: We give a rigorous characterization of what it means for a programming language to be memory safe, capturing the intuition that memory safety supports local reasoning about state. We formalize this principle in two ways. First, we show how a small memory-safe language validates a noninterference property: a program can neither affect nor be affected by unreachable parts of the state. Second, we ex… ▽ More We give a rigorous characterization of what it means for a programming language to be memory safe, capturing the intuition that memory safety supports local reasoning about state. We formalize this principle in two ways. First, we show how a small memory-safe language validates a noninterference property: a program can neither affect nor be affected by unreachable parts of the state. Second, we extend separation logic, a proof system for heap-manipulating programs, with a memory-safe variant of its frame rule. The new rule is stronger because it applies even when parts of the program are buggy or malicious, but also weaker because it demands a stricter form of separation between parts of the program state. We also consider a number of pragmatically motivated variations on memory safety and the reasoning principles they support. As an application of our characterization, we evaluate the security of a previously proposed dynamic monitor for memory safety of heap-allocated data. △ Less

Submitted 6 April, 2018; v1 submitted 20 May, 2017; originally announced May 2017.

Comments: POST'18 final version

Star formation histories in mergers: The spatially resolved properties of the early-stage merger LIRGs IC 1623 and NGC 6090

Authors: C. Cortijo-Ferrero, R. M. González Delgado, E. Pérez, R. Cid Fernandes, S. F. Sánchez, A. L. de Amorim, P. Di Matteo, R. García-Benito, E. A. D. Lacerda, R. López Fernández, C. Tadhunter

Abstract: The role of major mergers in galaxy evolution is investigated through a detailed characterization of the stellar populations, ionized gas properties, and star formation rates (SFR) in the early-stage merger LIRGs IC 1623 W and NGC 6090, by analysing optical Integral Field Spectroscopy (IFS) and high resolution HST imaging. The spectra were processed with the Starlight full spectral fitting code, a… ▽ More The role of major mergers in galaxy evolution is investigated through a detailed characterization of the stellar populations, ionized gas properties, and star formation rates (SFR) in the early-stage merger LIRGs IC 1623 W and NGC 6090, by analysing optical Integral Field Spectroscopy (IFS) and high resolution HST imaging. The spectra were processed with the Starlight full spectral fitting code, and the emission lines measured in the residual spectra. The results are compared with control non-interacting spiral galaxies from the CALIFA survey. Merger-induced star formation is extended and recent, as revealed by the young ages (50-80 Myr) and high contributions to light of young stellar populations (50-90$\%$), in agreement with merger simulations in the literature. These early-stage mergers have positive central gradients of the stellar metallicity, with an average $\sim$0.6 Z$_{\odot}$. Compared to non-interacting spirals, they have lower central nebular metallicity, and flatter profiles, in agreement with the gas inflow scenario. We find that they are dominated by star formation, although shock excitation cannot be discarded in some regions, where high velocity dispersion is found (170-200 km s$^{-1}$). The average SFR in these early-stage mergers ($\sim$23-32 M$_{\odot}$ yr$^{-1}$) is enhanced with respect to main-sequence Sbc galaxies by factors of 6-9, slightly above the predictions from classical merger simulations, but still possible in about 15$\%$ of major galaxy mergers, where U/LIRGs belong. △ Less

Submitted 21 February, 2017; originally announced February 2017.

Journal ref: MNRAS, 467, 3898-3919 (2017)

A Semantic Account of Metric Preservation

Authors: Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, Ikram Cherigui

Abstract: Program sensitivity measures how robust a program is to small changes in its input, and is a fundamental notion in domains ranging from differential privacy to cyber-physical systems. A natural way to formalize program sensitivity is in terms of metrics on the input and output spaces, requiring that an $r$-sensitive function map inputs that are at distance $d$ to outputs that are at distance at mo… ▽ More Program sensitivity measures how robust a program is to small changes in its input, and is a fundamental notion in domains ranging from differential privacy to cyber-physical systems. A natural way to formalize program sensitivity is in terms of metrics on the input and output spaces, requiring that an $r$-sensitive function map inputs that are at distance $d$ to outputs that are at distance at most $r \cdot d$. Program sensitivity is thus an analogue of Lipschitz continuity for programs. Reed and Pierce introduced Fuzz, a functional language with a linear type system that can express program sensitivity. They show soundness operationally, in the form of a metric preservation property. Inspired by their work, we study program sensitivity and metric preservation from a denotational point of view. In particular, we introduce metric CPOs, a novel semantic structure for reasoning about computation on metric spaces, by endowing CPOs with a compatible notion of distance. This structure is useful for reasoning about metric properties of programs, and specifically about program sensitivity. We demonstrate metric CPOs by giving a model for the deterministic fragment of Fuzz. △ Less

Submitted 23 October, 2022; v1 submitted 1 February, 2017; originally announced February 2017.

Star formation along the Hubble sequence: Radial structure of the star formation of CALIFA galaxies

Authors: R. M. González Delgado, R. Cid Fernandes, E. Pérez, R. García-Benito, R. López Fernández, E. A. D. Lacerda, C. Cortijo-Ferrero, A. L. de Amorim, N. Vale Asari, S. F. Sánchez, C. J. Walcher, L. Wisotzki, D. Mast, J. Alves, Y. Ascasibar, J. Bland-Hawthorn, L. Galbany, R. C. Kennicutt Jr., I. Márquez, J. Masegosa, M. Mollá, P. Sánchez-Blázquez, J. M. Vílchez, CALIFA collaboration

Abstract: The aim of this paper is to characterize the radial structure of the star formation rate (SFR) in galaxies in the nearby Universe as represented by the CALIFA survey. The sample under study contains 416 galaxies observed with IFS, covering a wide range of Hubble types and stellar masses. Spectral synthesis techniques are applied to obtain radial profiles of the intensity of the star formation rate… ▽ More The aim of this paper is to characterize the radial structure of the star formation rate (SFR) in galaxies in the nearby Universe as represented by the CALIFA survey. The sample under study contains 416 galaxies observed with IFS, covering a wide range of Hubble types and stellar masses. Spectral synthesis techniques are applied to obtain radial profiles of the intensity of the star formation rate in the recent past, and the local sSFR. To emphasize the behavior of these properties for galaxies that are on and off the main sequence of star formation (MSSF) we stack the individual radial profiles in bins of galaxy morphology and stellar masses. Our main results are: a) The intensity of SFR shows declining profiles that exhibit very little differences between spirals. The dispersion between the profiles is significantly smaller in late type spirals. This confirms that the MSSF is a sequence of galaxies with nearly constant intensity of SFR b) sSFR values scale with Hubble type and increase radially outwards, with a steeper slope in the inner 1 HLR. This behavior suggests that galaxies are quenched inside-out, and that this process is faster in the central, bulge-dominated part than in the disks. c) As a whole, and at all radii, E and S0 are off the MSSF. d) Applying the volume-corrections for the CALIFA sample, we obtain a density of star formation in the local Universe of 0.0105 Msun/yr/Mpc^{-3}. Most of the star formation is occurring in the disks of spirals. e) The volume averaged birthrate parameter, b'=0.39, suggests that the present day Universe is forming stars at 1/3 of its past average rate. E, S0, and the bulge of early type spirals contribute little to the recent SFR of the Universe, which is dominated by the disks of later spirals. f) There is a tight relation between the intensity of the SFR and stellar mass, defining a local MSSF relation with a logarithmic slope of 0.8. △ Less

Submitted 2 March, 2016; originally announced March 2016.

Comments: 17 pages, 11 figures, accepted for publication in Astronomy & Astrophysics. Abridged abstract

Beyond Good and Evil: Formalizing the Security Guarantees of Compartmentalizing Compilation

Authors: Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Boris Eng, Benjamin C. Pierce

Abstract: Compartmentalization is good security-engineering practice. By breaking a large software system into mutually distrustful components that run with minimal privileges, restricting their interactions to conform to well-defined interfaces, we can limit the damage caused by low-level attacks such as control-flow hijacking. When used to defend against such attacks, compartmentalization is often impleme… ▽ More Compartmentalization is good security-engineering practice. By breaking a large software system into mutually distrustful components that run with minimal privileges, restricting their interactions to conform to well-defined interfaces, we can limit the damage caused by low-level attacks such as control-flow hijacking. When used to defend against such attacks, compartmentalization is often implemented cooperatively by a compiler and a low-level compartmentalization mechanism. However, the formal guarantees provided by such compartmentalizing compilation have seen surprisingly little investigation. We propose a new security property, secure compartmentalizing compilation (SCC), that formally characterizes the guarantees provided by compartmentalizing compilation and clarifies its attacker model. We reconstruct our property by starting from the well-established notion of fully abstract compilation, then identifying and lifting three important limitations that make standard full abstraction unsuitable for compartmentalization. The connection to full abstraction allows us to prove SCC by adapting established proof techniques; we illustrate this with a compiler from a simple unsafe imperative language with procedures to a compartmentalized abstract machine. △ Less

Submitted 15 April, 2017; v1 submitted 14 February, 2016; originally announced February 2016.

Comments: Nits

Simultaneous spectroscopic and photometric analysis of galaxies with STARLIGHT: CALIFA $+$ GALEX

Authors: R. López Fernández, R. Cid Fernandes, R. M. González Delgado, N. Vale Asari, E. Pérez, R. García-Benito, A. L. de Amorim, E. A. D. Lacerda, C. Cortijo-Ferrero, S. F. Sánchez

Abstract: We present an extended version of the spectral synthesis code STARLIGHT designed to incorporate both $λ$-by-$λ$ spectra and photometric fluxes in the estimation of stellar population properties of galaxies. The code is tested with simulations and data for 260 galaxies culled from the CALIFA survey, spatially matching the 3700--7000 Å optical datacubes to GALEX near and far UV images. The sample sp… ▽ More We present an extended version of the spectral synthesis code STARLIGHT designed to incorporate both $λ$-by-$λ$ spectra and photometric fluxes in the estimation of stellar population properties of galaxies. The code is tested with simulations and data for 260 galaxies culled from the CALIFA survey, spatially matching the 3700--7000 Å optical datacubes to GALEX near and far UV images. The sample spans E--Sd galaxies with masses from $10^9$ to $10^{12} M_\odot$ and stellar populations all the way from star-forming to old, passive systems. Comparing results derived from purely optical fits with those which also consider the NUV and FUV data we find that: (1) The new code is capable of matching the input UV data within the errors while keeping the quality of the optical fit essentially unchanged. (2) Despite being unreliable predictors of the UV fluxes, purely optical fits yield stellar population properties which agree well with those obtained in optical+UV fits for nearly 90% of our sample. (3) The addition of UV constraints has little impact on properties such as stellar mass and dust optical depth. Mean stellar ages and metallicities also remain nearly the same for most galaxies, the exception being low-mass, late-type galaxies, which become older and less enriched due to rearrangements of their youngest populations. (4) The revised ages are better correlated with observables such as the 4000 Å break index, and the $NUV - r$ and $u - r$ colours, an empirical indication that the addition of UV constraints helps mitigating the effects of age-metallicity-extinction degeneracies. △ Less

Submitted 2 February, 2016; originally announced February 2016.

Comments: Accepted for publication in MNRAS 2016 January 28, 18 pages, 14 figures, 3 tables

Towards a Fully Abstract Compiler Using Micro-Policies: Secure Compilation for Mutually Distrustful Components

Authors: Yannis Juglaret, Catalin Hritcu, Arthur Azevedo de Amorim, Benjamin C. Pierce, Antal Spector-Zabusky, Andrew Tolmach

Abstract: Secure compilation prevents all low-level attacks on compiled code and allows for sound reasoning about security in the source language. In this work we propose a new attacker model for secure compilation that extends the well-known notion of full abstraction to ensure protection for mutually distrustful components. We devise a compiler chain (compiler, linker, and loader) and a novel security mon… ▽ More Secure compilation prevents all low-level attacks on compiled code and allows for sound reasoning about security in the source language. In this work we propose a new attacker model for secure compilation that extends the well-known notion of full abstraction to ensure protection for mutually distrustful components. We devise a compiler chain (compiler, linker, and loader) and a novel security monitor that together defend against this strong attacker model. The monitor is implemented using a recently proposed, generic tag-based protection framework called micro-policies, which comes with hardware support for efficient caching and with a formal verification methodology. Our monitor protects the abstractions of a simple object-oriented language---class isolation, the method call discipline, and type safety---against arbitrary low-level attackers. △ Less

Submitted 2 October, 2015; originally announced October 2015.

A Verified Information-Flow Architecture

Authors: Arthur Azevedo de Amorim, Nathan Collins, André DeHon, Delphine Demange, Catalin Hritcu, David Pichardie, Benjamin C. Pierce, Randy Pollack, Andrew Tolmach

Abstract: SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supports fine-grained programmable tags, with efficient and flexible propagation and combination of tags as instructions are executed. The operating system virtualizes these generic facilities to present an information-flow… ▽ More SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supports fine-grained programmable tags, with efficient and flexible propagation and combination of tags as instructions are executed. The operating system virtualizes these generic facilities to present an information-flow abstract machine that allows user programs to label sensitive data with rich confidentiality policies. We present a formal, machine-checked model of the key hardware and software mechanisms used to dynamically control information flow in SAFE and an end-to-end proof of noninterference for this model. We use a refinement proof methodology to propagate the noninterference property of the abstract machine down to the concrete machine level. We use an intermediate layer in the refinement chain that factors out the details of the information-flow control policy and devise a code generator for compiling such information-flow policies into low-level monitor code. Finally, we verify the correctness of this generator using a dedicated Hoare logic that abstracts from low-level machine instructions into a reusable set of verified structured code generators. △ Less

Submitted 6 March, 2016; v1 submitted 22 September, 2015; originally announced September 2015.

The CALIFA survey across the Hubble sequence: Spatially resolved stellar population properties in galaxies

Authors: R. M. González Delgado, R. García-Benito, E. Pérez, R. Cid Fernandes, A. L. de Amorim, C. Cortijo-Ferrero, E. A. D. Lacerda, R. López Fernández, N. Vale-Asari, S. F. Sánchez, M. Mollá, T. Ruiz-Lara, P. Sánchez-Blázquez, C. J. Walcher, J. Alves, J. A. L. Aguerri, S. Bekeraité, J. Bland-Hawthorn, L. Galbany, A. Gallazzi, B. Husemann, J. Iglesias-Páramo, V. Kalinova, A. R. López-Sánchez, R. A. Marino , et al. (10 additional authors not shown)

Abstract: This paper characterizes the radial structure of stellar population properties of galaxies in the nearby universe, based on 300 galaxies from the CALIFA survey. The sample covers a wide range of Hubble types, and galaxy stellar mass. We apply the spectral synthesis techniques to recover the stellar mass surface density, stellar extinction, light and mass-weighted ages, and mass-weighted metallicit… ▽ More This paper characterizes the radial structure of stellar population properties of galaxies in the nearby universe, based on 300 galaxies from the CALIFA survey. The sample covers a wide range of Hubble types, and galaxy stellar mass. We apply the spectral synthesis techniques to recover the stellar mass surface density, stellar extinction, light and mass-weighted ages, and mass-weighted metallicity, for each spatial resolution element in our target galaxies. To study mean trends with overall galaxy properties, the individual radial profiles are stacked in seven bins of galaxy morphology. We confirm that more massive galaxies are more compact, older, more metal rich, and less reddened by dust. Additionally, we find that these trends are preserved spatially with the radial distance to the nucleus. Deviations from these relations appear correlated with Hubble type: earlier types are more compact, older, and more metal rich for a given mass, which evidences that quenching is related to morphology, but not driven by mass. Negative gradients of ages are consistent with an inside-out growth of galaxies, with the largest ages gradients in Sb-Sbc galaxies. Further, the mean stellar ages of disks and bulges are correlated, with disks covering a wider range of ages, and late type spirals hosting younger disks. The gradients in stellar mass surface density depend mostly on stellar mass, in the sense that more massive galaxies are more centrally concentrated. There is a secondary correlation in the sense that at the same mass early type galaxies have steeper gradients. We find mildly negative metallicity gradients, shallower than predicted from models of galaxy evolution in isolation. The largest gradients occur in Sb galaxies. Overall we conclude that quenching processes act in manners that are independent of mass, while metallicity and galaxy structure are influenced by mass-dependent processes. △ Less

Submitted 16 June, 2015; v1 submitted 12 June, 2015; originally announced June 2015.

Comments: 42 pages, 27 figures, 3 tables. Abridged abstract for arXiv. Accepted for publication in A&A

The CALIFA survey across the Hubble sequence: How galaxies grow their bulges and disks

Authors: R. M. González Delgado, R. García-Benito, E. Pérez, R. Cid Fernandes, A. L. de Amorim, C. Cortijo-Ferrero, E. A. D. Lacerda, R. López Fernández, N. Vale-Asari, S. Sánchez, CALIFA collaboration

Abstract: We characterize in detail the radial structure of the stellar population properties of 300 galaxies in the nearby universe, observed with integral field spectroscopy in the CALIFA survey. The sample covers a wide range of Hubble types, from spheroidal to spiral galaxies, ranging in stellar masses from $M_\star \sim 10^9$ to $7 \times 10^{11}$ $M_\odot$. We derive the stellar mass surface density (… ▽ More We characterize in detail the radial structure of the stellar population properties of 300 galaxies in the nearby universe, observed with integral field spectroscopy in the CALIFA survey. The sample covers a wide range of Hubble types, from spheroidal to spiral galaxies, ranging in stellar masses from $M_\star \sim 10^9$ to $7 \times 10^{11}$ $M_\odot$. We derive the stellar mass surface density ($μ_\star$), light-weighted and mass-weighted ages ($\langle {\rm log}\,age\rangle _L$, $\langle {\rm log}\,age\rangle _M$), and mass-weighted metallicity ($\langle {\rm log}\,Z_\star\rangle _M$), applying the spectral synthesis technique. We study the mean trends with galaxy stellar mass, $M_\star$, and morphology (E, S0, Sa, Sb, Sbc, Sc and Sd). We confirm that more massive galaxies are more compact, older, more metal rich, and less reddened by dust. Additionally, we find that these trends are preserved spatially with the radial distance to the nucleus. Deviations from these relations appear correlated with Hubble type: earlier types are more compact, older, and more metal rich for a given M$_\star$, which evidences that quenching is related to morphology, but not driven by mass. △ Less

Submitted 9 June, 2015; originally announced June 2015.

Comments: 5 pages, 3 figures, Proceedings for "Multi-Object Spectroscopy in the Next Decade: Big Questions, Large Surveys and Wide Fields", Santa Cruz de La Palma, Canary Islands, 2nd to 6th March 2015