Zobrazeno 1 - 10
of 100
pro vyhledávání: '"Aaron Stump"'
Autor:
Aaron Stump
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 307, Iss Proc. LFMTP 2019, Pp 55-67 (2019)
Cedille is a relatively recent tool based on a Curry-style pure type theory, without a primitive datatype system. Using novel techniques based on dependent intersection types, inductive datatypes with their induction principles are derived. One benef
Externí odkaz:
https://doaj.org/article/cd381c294b414b9180f4329838caf4ff
Publikováno v:
Logical Methods in Computer Science, Vol Volume 12, Issue 3 (2017)
We propose a new bi-intuitionistic type theory called Dualized Type Theory (DTT). It is a simple type theory with perfect intuitionistic duality, and corresponds to a single-sided polarized sequent calculus. We prove DTT strongly normalizing, and pro
Externí odkaz:
https://doaj.org/article/690a39d17ca848c3adf13c6d45322289
Autor:
Harley Eades, Aaron Stump
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 127, Iss Proc. COS 2013, Pp 45-65 (2013)
Hereditary substitution is a form of type-bounded iterated substitution, first made explicit by Watkins et al. and Adams in order to show normalization of proof terms for various constructive logics. This paper is the first to apply hereditary substi
Externí odkaz:
https://doaj.org/article/18477d715167404fafbb09e87a39adc6
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
Autor:
Vilhelm Sjöberg, Aaron Stump
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 45, Iss Proc. ITRS 2010, Pp 90-100 (2011)
This paper presents a type theory with a form of equality reflection: provable equalities can be used to coerce the type of a term. Coercions and other annotations, including implicit arguments, are dropped during reduction of terms. We develop the m
Externí odkaz:
https://doaj.org/article/ff62fa4a473c43e2a65a8a3bde126e70
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
Publikováno v:
Logical Methods in Computer Science, Vol Volume 9, Issue 1 (2013)
This paper shows how a recently developed view of typing as small-step abstract reduction, due to Kuan, MacQueen, and Findler, can be used to recast the development of simple type theory from a rewriting perspective. We show how standard meta-theoret
Externí odkaz:
https://doaj.org/article/d40f4a87ee974ec49b33523587023d48
This paper proposes a new approach to writing and verifying divide-and-conquer programs in Coq. Extending the rich line of previous work on algebraic approaches to recursion schemes, we present an algebraic approach to divide-and-conquer recursion: r
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3a1f9f716034c9aac5101080385adb47
Publikováno v:
Proceedings of the ACM on Programming Languages. 4:1-25
This paper describes an implementation of Harper's continuation-based regular-expression matcher as a strong functional program in Cedille; i.e., Cedille statically confirms termination of the program on all inputs. The approach uses neither dependen
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::dea4b3e286a07495ccb5493f277f7aad
https://doi.org/10.1145/3409004
https://doi.org/10.1145/3409004
Publikováno v:
IFL
Constructor subtyping is a form of subtyping where two inductive types can be related as long as the inductive signature of one is a subsignature of the other. To be a subsignature requires every constructor of the smaller datatype be present in the
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2e016abbbf3d6c8707c0f8cbecb8c14f
https://doi.org/10.1145/3462172.3462194
https://doi.org/10.1145/3462172.3462194