Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userOn the Soundness of Coroutines with Snapshots
107
0
0.0
(
0
)
Added by
Aleksandar Prokopec
Publication date
2018
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Coroutines are a general control flow construct that can eliminate control flow fragmentation inherent in event-driven programs, and are still missing in many popular languages. Coroutines with snapshots are a first-class, type-safe, stackful coroutine model, which unifies many variants of suspendable computing, and is sufficiently general to express iterators, single-assignment variables, async-await, actors, event streams, backtracking, symmetric coroutines and continuations. In this paper, we develop a formal model called $lambda_{rightsquigarrow}$ (lambda-squiggly) that captures the essence of type-safe, stackful, delimited coroutines with snapshots. We prove the standard progress and preservation safety properties. Finally, we show a formal transformation from the $lambda_{rightsquigarrow}$ calculus to the simply-typed lambda calculus with references.
rate research
Read More
Scalas type system unifies ML modules, object-oriented, and functional programming. The Dependent Object Types (DOT) family of calculi has been proposed as a new foundation for Scala and similar languages. Unfortunately, it is not clear how DOT relates to any well-known type systems, and type soundness has only been established for very restricted subsets. In fact, important Scala features are known to break at least one key metatheoretic property such as environment narrowing or subtyping transitivity, which are usually required for a type soundness proof. First, and, perhaps surprisingly, we show how rich DOT calculi can still be proved sound. The key insight is that narrowing and subtyping transitivity only need to hold for runtime objects, but not for code that is never executed. Alas, the dominant method of proving type soundness, Wright and Felleisens syntactic approach, is based on term rewriting, which does not a priori make a distinction between runtime and type assignment time. Second, we demonstrate how type soundness can be proved for advanced, polymorphic, type systems with respect to high-level, definitional interpreters, implemented in Coq. We present the first mechanized soundness proof in this style for System F<: and several extensions, including mutable references. Our proofs use only simple induction: another surprising result, as the combination of big-step semantics, mutable references, and polymorphism is commonly believed to require co-inductive proof techniques. Third, we show how DOT-like calculi emerge as generalizations of F<:, exposing a rich design space of calculi with path-dependent types which we collectively call System D. Armed with insights from the definitional interpreter semantics, we also show how equivalent small-step semantics and soundness proofs in Wright-Felleisen-style can be derived for these systems.
We propose a general proof technique to show that a predicate is sound, that is, prevents stuck computation, with respect to a big-step semantics. This result may look surprising, since in big-step semantics there is no difference between non-terminating and stuck computations, hence soundness cannot even be expressed. The key idea is to define constructions yielding an extended version of a given arbitrary big-step semantics, where the difference is made explicit. The extended semantics are exploited in the meta-theory, notably they are necessary to show that the proof technique works. However, they remain transparent when using the proof technique, since it consists in checking three conditions on the original rules only, as we illustrate by several examples.
In this paper we continue the study, from Frittaion, Steila and Yokoyama (2017), on size-change termination in the context of Reverse Mathematics. We analyze the soundness of the SCT method. In particular, we prove that the statement any program which satisfies the combinatorial condition provided by the SCT criterion is terminating is equivalent to $mathrm{WO}(omega_3)$ over $mathsf{RCA_0}$
Type Ia Supernovae (SNeIa) used as standardizable candles have been instrumental in the discovery of cosmic acceleration, usually attributed to some form of dark energy (DE). Recent studies have raised the issue of whether intrinsic SNeIa luminosities might evolve with redshift. While the evidence for cosmic acceleration is robust to this possible systematic, the question remains of how much the latter can affect the inferred properties of the DE component responsible for cosmic acceleration. This is the question we address in this work. We use SNeIa distance moduli measurements from the Pantheon and JLA samples. We consider models where the DE equation of state is a free parameter, either constant or time-varying, as well as models where DE and dark matter interact, and finally a model-agnostic parametrization of effects due to modified gravity (MG). When SNeIa data are combined with Cosmic Microwave Background (CMB) temperature and polarization anisotropy measurements, we find strong degeneracies between parameters governing the SNeIa systematics, the DE parameters, and the Hubble constant $H_0$. These degeneracies significantly broaden the DE parameter uncertainties, in some cases leading to ${cal O}(sigma)$ shifts in the central values. However, including low-redshift Baryon Acoustic Oscillation and Cosmic Chronometer measurements, as well as CMB lensing measurements, considerably improves the previous constraints, and the only remaining effect of the examined systematic is a $lesssim 40%$ broadening of the uncertainties on the DE parameters. The constraints we derive on the MG parameters are instead basically unaffected by the systematic in question. We therefore confirm the overall soundness of dark energy properties.
We present an update of our on-going project to characterise the impact of radio jets on the ISM by tracing molecular gas at high spatial resolution using ALMA. The radio active galactic nuclei (AGN) studied show recently born radio jets. In this stage, the plasma jets can have the largest impact on the ISM, as also predicted by state-of-the-art simulations. The two targets have quite different ages, allowing us to get snapshots of the effects of radio jets as they grow. Interestingly, both also host powerful quasar emission. The largest mass outflow rate of molecular gas is found in a radio galaxy hosting a newly born radio jet emerging from an obscuring cocoon of gas and dust. Although the mass outflow rate is high (few hundred Msun/yr), the outflow is limited to the inner few hundred pc region. In a second object, the jet is larger (a few kpc) and is in a more advanced evolutionary phase. In this object, the distribution of the molecular gas is reminiscent of what is seen, on larger scales, in cool-core clusters hosting radio galaxies. Gas deviating from quiescent kinematics is not very prominent, limited only to the very inner region, and has a low mass outflow rate. Instead, on kpc scales, the radio lobes appear associated with depressions in the distribution of the molecular gas, suggesting they have broken out from the dense nuclear region. The AGN does not appear to be able at present to stop the star formation observed in this galaxy. These results suggest that the effects of the radio source start in the first phases by producing outflows which, however, tend to be limited to the kpc region. After that, the effects turn into producing large-scale bubbles which could, in the long term, prevent the surrounding gas from cooling. Our results characterise the effect of radio jets in different phases of their evolution, bridging the studies done for radio galaxies in clusters.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
