Zobrazeno 1 - 10
of 81
pro vyhledávání: '"Stephanie Weirich"'
Autor:
Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 76, Iss Proc. MSFP 2012, Pp 112-162 (2012)
We present a full-spectrum dependently typed core language which includes both nontermination and computational irrelevance (a.k.a. erasure), a combination which has not been studied before. The two features interact: to protect type safety we must b
Externí odkaz:
https://doaj.org/article/377d50b72b4a4b8fa419a7776956326a
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 76, Iss Proc. MSFP 2012, Pp 25-39 (2012)
The Trellys project has produced several designs for practical dependently typed languages. These languages are broken into two fragments—a _logical_ fragment where every term normalizes and which is consistent when interpreted as a logic, and a _p
Externí odkaz:
https://doaj.org/article/4d24bda3067b433bad3c0fa99e8d0e9f
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 43, Iss Proc. PAR 2010, Pp 76-93 (2010)
This paper proposes a type-and-effect system called Teqt, which distinguishes terminating terms and total functions from possibly diverging terms and partial functions, for a lambda calculus with general recursion and equality types. The central idea
Externí odkaz:
https://doaj.org/article/689ed5c93b9f497b8e5ad57de25e7fc9
Autor:
Stephanie Weirich
The two-volume open access book set LNCS 14576 + 14577 constitutes the proceedings of the 33rd European Symposium on Programming, ESOP 2024, which was held during April 6-11, 2024, in Luxemburg, as part of the European Joint Conferences on Theory and
Autor:
Yao Li, Stephanie Weirich
Publikováno v:
Proceedings of the ACM on Programming Languages. 6:312-342
Free monads (and their variants) have become a popular general-purpose tool for representing the semantics of effectful programs in proof assistants. These data structures support the compositional definition of semantics parameterized by uninterpret
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5e10261330be641a7677b83661eb2254
https://doi.org/10.1145/3547632
https://doi.org/10.1145/3547632
Publikováno v:
Proceedings of the ACM on Programming Languages. 5:1-29
Despite the great success of inferring and programming with universal types, their dual—existential types—are much harder to work with. Existential types are useful in building abstract types, working with indexed types, and providing first-class
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6edcf9001055694f2a32d22d7b5d7d28
https://doi.org/10.1145/3473569
https://doi.org/10.1145/3473569
Publikováno v:
Proceedings of the ACM on Programming Languages. 5:1-32
Graded Type Theory provides a mechanism to track and reason about resource usage in type systems. In this paper, we develop GraD, a novel version of such a graded dependent type system that includes functions, tensor products, additive sums, and a un
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4d8138a8b805697131f69d03e3bb4dd4
https://doi.org/10.1145/3434331
https://doi.org/10.1145/3434331
Publikováno v:
Programming Languages and Systems ISBN: 9783030993351
Over twenty years ago, Abadi et al. established the Dependency Core Calculus (DCC) as a general purpose framework for analyzing dependency in typed programming languages. Since then, dependency analysis has shown many practical benefits to language d
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::506ffe3bb0fa079022d3fdec6c46e1dd
https://doi.org/10.1007/978-3-030-99336-8_15
https://doi.org/10.1007/978-3-030-99336-8_15
Publikováno v:
Proceedings of the ACM on Programming Languages. 3:1-29
Modern Haskell supports zero-cost coercions, a mechanism where types that share the same run-time representation may be freely converted between. To make sure such conversions are safe and desirable, this feature relies on a mechanism of roles to pro
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2c8ec1eefde639c6a24e84bbec329c63
https://doi.org/10.1145/3341705
https://doi.org/10.1145/3341705
Publikováno v:
Li, Y, Xia, L & Weirich, S 2021, ' Reasoning about the Garden of Forking Paths ', Proceedings of the ACM on Programming Languages, vol. 5, no. ICFP, 80 . https://doi.org/10.1145/3473585
Lazy evaluation is a powerful tool for functional programmers. It enables the concise expression of on-demand computation and a form of compositionality not available under other evaluation strategies. However, the stateful nature of lazy evaluation
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::753e3546328c4fcdc19f2795d0846370