skip to main content

Title: Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi
Abstract The research on gradual typing has led to many variations on the Gradually Typed Lambda Calculus (GTLC) of Siek & Taha (2006) and its underlying cast calculus. For example, Wadler and Findler (2009) added blame tracking, Siek et al . (2009) investigated alternate cast evaluation strategies, and Herman et al . (2010) replaced casts with coercions for space efficiency. The meta-theory for the GTLC has also expanded beyond type safety to include blame safety (Tobin-Hochstadt & Felleisen, 2006), space consumption (Herman et al ., 2010), and the gradual guarantees (Siek et al ., 2015). These results have been proven for some variations of the GTLC but not others. Furthermore, researchers continue to develop variations on the GTLC, but establishing all of the meta-theory for new variations is time-consuming. This article identifies abstractions that capture similarities between many cast calculi in the form of two parameterized cast calculi, one for the purposes of language specification and the other to guide space-efficient implementations. The article then develops reusable meta-theory for these two calculi, proving type safety, blame safety, the gradual guarantees, and space consumption. Finally, the article instantiates this meta-theory for eight cast calculi including five from the literature and three new calculi. All of these definitions and theorems, including the two parameterized calculi, the reusable meta-theory, and the eight instantiations, are mechanized in Agda making extensive use of module parameters and dependent records to define the abstractions.  more » « less
Award ID(s):
Author(s) / Creator(s):
Date Published:
Journal Name:
Journal of Functional Programming
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. By mimicking biomimetic synaptic processes, the success of artificial intelligence (AI) has been astounding with various applications such as driving automation, big data analysis, and natural-language processing.[1-4] Due to a large quantity of data transmission between the separated memory unit and the logic unit, the classical computing system with von Neumann architecture consumes excessive energy and has a significant processing delay.[5] Furthermore, the speed difference between the two units also causes extra delay, which is referred to as the memory wall.[6, 7] To keep pace with the rapid growth of AI applications, enhanced hardware systems that particularly feature an energy-efficient and high-speed hardware system need to be secured. The novel neuromorphic computing system, an in-memory architecture with low power consumption, has been suggested as an alternative to the conventional system. Memristors with analog-type resistive switching behavior are a promising candidate for implementing the neuromorphic computing system since the devices can modulate the conductance with cycles that act as synaptic weights to process input signals and store information.[8, 9]

    The memristor has sparked tremendous interest due to its simple two-terminal structure, including top electrode (TE), bottom electrode (BE), and an intermediate resistive switching (RS) layer. Many oxide materials, including HfO2, Ta2O5, and IGZO, have extensively been studied as an RS layer of memristors. Silicon dioxide (SiO2) features 3D structural conformity with the conventional CMOS technology and high wafer-scale homogeneity, which has benefited modern microelectronic devices as dielectric and/or passivation layers. Therefore, the use of SiO2as a memristor RS layer for neuromorphic computing is expected to be compatible with current Si technology with minimal processing and material-related complexities.

    In this work, we proposed SiO2-based memristor and investigated switching behaviors metallized with different reduction potentials by applying pure Cu and Ag, and their alloys with varied ratios. Heavily doped p-type silicon was chosen as BE in order to exclude any effects of the BE ions on the memristor performance. We previously reported that the selection of TE is crucial for achieving a high memory window and stable switching performance. According to the study which compares the roles of Cu (switching stabilizer) and Ag (large switching window performer) TEs for oxide memristors, we have selected the TE materials and their alloys to engineer the SiO2-based memristor characteristics. The Ag TE leads to a larger memory window of the SiO2memristor, but the device shows relatively large variation and less reliability. On the other hand, the Cu TE device presents uniform gradual switching behavior which is in line with our previous report that Cu can be served as a stabilizer, but with small on/off ratio.[9] These distinct performances with Cu and Ag metallization leads us to utilize a Cu/Ag alloy as the TE. Various compositions of Cu/Ag were examined for the optimization of the memristor TEs. With a Cu/Ag alloying TE with optimized ratio, our SiO2based memristor demonstrates uniform switching behavior and memory window for analog switching applications. Also, it shows ideal potentiation and depression synaptic behavior under the positive/negative spikes (pulse train).

    In conclusion, the SiO2memristors with different metallization were established. To tune the property of RS layer, the sputtering conditions of RS were varied. To investigate the influence of TE selections on switching performance of memristor, we integrated Cu, Ag and Cu/Ag alloy as TEs and compared the switch characteristics. Our encouraging results clearly demonstrate that SiO2with Cu/Ag is a promising memristor device with synaptic switching behavior in neuromorphic computing applications.


    This work was supported by the U.S. National Science Foundation (NSF) Award No. ECCS-1931088. S.L. and H.W.S. acknowledge the support from the Improvement of Measurement Standards and Technology for Mechanical Metrology (Grant No. 22011044) by KRISS.


    [1] Younget al.,IEEE Computational Intelligence Magazine,vol. 13, no. 3, pp. 55-75, 2018.

    [2] Hadsellet al.,Journal of Field Robotics,vol. 26, no. 2, pp. 120-144, 2009.

    [3] Najafabadiet al.,Journal of Big Data,vol. 2, no. 1, p. 1, 2015.

    [4] Zhaoet al.,Applied Physics Reviews,vol. 7, no. 1, 2020.

    [5] Zidanet al.,Nature Electronics,vol. 1, no. 1, pp. 22-29, 2018.

    [6] Wulfet al.,SIGARCH Comput. Archit. News,vol. 23, no. 1, pp. 20–24, 1995.

    [7] Wilkes,SIGARCH Comput. Archit. News,vol. 23, no. 4, pp. 4–6, 1995.

    [8] Ielminiet al.,Nature Electronics,vol. 1, no. 6, pp. 333-343, 2018.

    [9] Changet al.,Nano Letters,vol. 10, no. 4, pp. 1297-1301, 2010.

    [10] Qinet al., Physica Status Solidi (RRL) - Rapid Research Letters, pssr.202200075R1, In press, 2022.

    more » « less
  2. The Baltimore Ecosystem Study (BES) has established a network of long-term permanent biogeochemical study plots. These plots will provide long-term data on vegetation, soil and hydrologic processes in the key ecosystem types within the urban ecosystem. The current network of study plots includes eight forest plots, chosen to represent the range of forest conditions in the area, and four grass plots. These plots are complemented by a network of 200 less intensive study plots located across the Baltimore metropolitan area. Plots are currently instrumented with lysimeters (drainage and tension) to sample soil solution chemistry, time domain reflectometry probes to measure soil moisture, dataloggers to measure and record soil temperature and trace gas flux chambers to measure the flux of carbon dioxide, nitrous oxide and methane from soil to the atmosphere. Measurements of in situ nitrogen mineralization, nitrification and denitrification were made at approximately monthly intervals from Fall 1998 - Fall 2000. Detailed vegetation characterization (all layers) was done in summer 1998. Data from these plots has been published in Groffman et al. (2006, 2009) and Groffman and Pouyat (2009). In November of 1998 four rural, forested plots were established at Oregon Ridge Park in Baltimore County northeast of the Gwynns Falls Watershed. Oregon Ridge Park contains Pond Branch, the forested reference watershed for BES. Two of these four plots are located on the top of a slope; the other two are located midway up the slope. In June of 2010 measurements at the mid-slope sites on Pond Branch were discontinued. Monuments and equipment remain at the two plots. These plots were replaced with two lowland riparian plots; Oregon upper riparian and Oregon lower riparian. Each riparian sites has four 5 cm by 1-2.5 meter depth slotted wells laid perpendicular to the stream, four tension lysimeters at 10 cm depth, five time domain reflectometry probes, and four trace gas flux chambers in the two dominant microtopographic features of the riparian zones - high spots (hummocks) and low spots (hollows). Four urban, forested plots were established in November 1998, two at Leakin Park and two adjacent to Hillsdale Park in west Baltimore City in the Gwynns Falls. One of the plots in Hillsdale Park was abandoned in 2004 due to continued vandalism. In May 1999 two grass, lawn plots were established at McDonogh School in Baltimore County west of the city in the Gwynns Falls. One of these plots is an extremely low intensity management area (mowed once or twice a year) and one is in a low intensity management area (frequent mowing, no fertilizer or herbicide use). In 2009, the McDonogh plots were abandoned due to management changes at the school. Two grass lawn plots were established on the campus of the University of Maryland, Baltimore County (UMBC) in fall 2000. One of these plots is in a medium intensity management area (frequent mowing, moderate applications of fertilizer and herbicides) and one is in a high intensity management area (frequent mowing, high applications of fertilizer and herbicides). Literature Cited Bowden R, Steudler P, Melillo J and Aber J. 1990. Annual nitrous oxide fluxes from temperate forest soils in the northeastern United States. J. Geophys. Res.-Atmos. 95, 13997 14005. Driscoll CT, Fuller RD and Simone DM (1988) Longitudinal variations in trace metal concentrations in a northern forested ecosystem. J. Environ. Qual. 17: 101-107 Goldman, M. B., P. M. Groffman, R. V. Pouyat, M. J. McDonnell, and S. T. A. Pickett. 1995. CH4 uptake and N availability in forest soils along an urban to rural gradient. Soil Biology and Biochemistry 27:281-286. Groffman PM, Holland E, Myrold DD, Robertson GP and Zou X (1999) Denitrification. In: Robertson GP, Bledsoe CS, Coleman DC and Sollins P (Eds) Standard Soil Methods for Long Term Ecological Research. (pp 272-290). Oxford University Press, New York Groffman PM, Pouyat RV, Cadenasso ML, Zipperer WC, Szlavecz K, Yesilonis IC,. Band LE and Brush GS. 2006. Land use context and natural soil controls on plant community composition and soil nitrogen and carbon dynamics in urban and rural forests. Forest Ecology and Management 236:177-192. Groffman, P.M., C.O. Williams, R.V. Pouyat, L.E. Band and I.C. Yesilonis. 2009. Nitrate leaching and nitrous oxide flux in urban forests and grasslands. Journal of Environmental Quality 38:1848-1860. Groffman, P.M. and R.V. Pouyat. 2009. Methane uptake in urban forests and lawns. Environmental Science and Technology 43:5229-5235. DOI: 10.1021/es803720h. Holland EA, Boone R, Greenberg J, Groffman PM and Robertson GP (1999) Measurement of Soil CO2, N2O and CH4 exchange. In: Robertson GP, Bledsoe CS, Coleman DC and Sollins P (Eds) Standard Soil Methods for Long Term Ecological Research. (pp 258-271). Oxford University Press, New York Robertson GP, Wedin D, Groffman PM, Blair JM, Holland EA, Nadelhoffer KJ and. Harris D. 1999. Soil carbon and nitrogen availability: Nitrogen mineralization, nitrification and carbon turnover. In: Standard Soil Methods for Long Term Ecological Research (Robertson GP, Bledsoe CS, Coleman DC and Sollins P (Eds) Standard Soil Methods for Long Term Ecological Research. (pp 258-271). Oxford University Press, New York Savva, Y., K. Szlavecz, R. V. Pouyat, P. M. Groffman, and G. Heisler. 2010. Effects of land use and vegetation cover on soil temperature in an urban ecosystem. Soil Science Society of America Journal 74:469-480." 
    more » « less
  3. null (Ed.)
    Abstract Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. Sound gradually typed languages dynamically check types at runtime at the boundary between statically typed and dynamically typed modules. However, there is much disagreement in the gradual typing literature over how to enforce complex types such as tuples, lists, functions and objects. In this paper, we propose a new perspective on the design of runtime gradual type enforcement: runtime type casts exist precisely to ensure the correctness of certain type-based refactorings and optimizations. For instance, for simple types, a language designer might desire that beta-eta equality is valid. We show that this perspective is useful by demonstrating that a cast semantics can be derived from beta-eta equality. We do this by providing an axiomatic account program equivalence in a gradual cast calculus in a logic we call gradual type theory (GTT). Based on Levy’s call-by-push-value, GTT allows us to axiomatize both call-by-value and call-by-name gradual languages. We then show that we can derive the behavior of casts for simple types from the corresponding eta equality principle and the assumption that the language satisfies a property called graduality , also known as the dynamic gradual guarantee. Since we can derive the semantics from the assumption of eta equality, we also receive a useful contrapositive: any observably different cast semantics that satisfies graduality must violate the eta equality. We show the consistency and applicability of our axiomatic theory by proving that a contract-based implementation using the lazy cast semantics gives a logical relations model of our type theory, where equivalence in GTT implies contextual equivalence of the programs. Since GTT also axiomatizes the dynamic gradual guarantee, our model also establishes this central theorem of gradual typing. The model is parameterized by the implementation of the dynamic types, and so gives a family of implementations that validate type-based optimization and the gradual guarantee. 
    more » « less
  4. Dependency analysis is vital to several applications in computer science. It lies at the essence of secure information flow analysis, binding-time analysis, etc. Various calculi have been proposed in the literature for analysing individual dependencies. Abadi et. al., by extending Moggi’s monadic metalanguage, unified several of these calculi into the Dependency Core Calculus (DCC). DCC has served as a foundational framework for dependency analysis for the last two decades. However, in spite of its success, DCC has its limitations. First, the monadic bind rule of the calculus is nonstandard and relies upon an auxiliary protection judgement. Second, being of a monadic nature, the calculus cannot capture dependency analyses that possess a comonadic nature, for example, the binding-time calculus, λ ∘ , of Davies. In this paper, we address these limitations by designing an alternative dependency calculus that is inspired by standard ideas from category theory. Our calculus is both monadic and comonadic in nature and subsumes both DCC and λ ∘ . Our construction explains the nonstandard bind rule and the protection judgement of DCC in terms of standard categorical concepts. It also leads to a novel technique for proving correctness of dependency analysis. We use this technique to present alternative proofs of correctness for DCC and λ ∘ . 
    more » « less
  5. Summary

    The usefulness of meta-analysis has been recognized in the evaluation of drug safety, as a single trial usually yields few adverse events and offers limited information. For rare events, conventional meta-analysis methods may yield an invalid inference, as they often rely on large sample theories and require empirical corrections for zero events. These problems motivate research in developing exact methods, including Tian et al.'s method of combining confidence intervals (2009, Biostatistics, 10, 275–281) and Liu et al.'s method of combining p-value functions (2014, JASA, 109, 1450–1465). This article shows that these two exact methods can be unified under the framework of combining confidence distributions (CDs). Furthermore, we show that the CD method generalizes Tian et al.'s method in several aspects. Given that the CD framework also subsumes the Mantel–Haenszel and Peto methods, we conclude that the CD method offers a general framework for meta-analysis of rare events. We illustrate the CD framework using two real data sets collected for the safety analysis of diabetes drugs.

    more » « less