اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدCocon: Computation in Contextual Type Theory
49
0
0.0
(
0
)
نشر من قبل
Francisco Ferreira Ruiz
تاريخ النشر
2019
مجال البحث
الهندسة المعلوماتية
والبحث باللغة
English
تأليف
Brigitte Pientka
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
We describe a Martin-Lof style dependent type theory, called Cocon, that allows us to mix the intensional function space that is used to represent higher-order abstract syntax (HOAS) trees with the extensional function space that describes (recursive) computations. We mediate between HOAS representations and computations using contextual modal types. Our type theory also supports an infinite hierarchy of universes and hence supports type-level computation -- thereby providing metaprogramming and (small-scale) reflection. Our main contribution is the development of a Kripke-style model for Cocon that allows us to prove normalization. From the normalization proof, we derive subject reduction and consistency. Our work lays the foundation to incorporate the methodology of logical frameworks into systems such as Agda and bridges the longstanding gap between these two worlds.
قيم البحث
اقرأ أيضاً
Although computational complexity is a fundamental aspect of program behavior, it is often at odds with common type theoretic principles such as function extensionality, which identifies all functions with the same $textit{input-output}$ behavior. We
present a computational type theory called $mathbf{CATT}$ that has a primitive notion of cost (the number of evaluation steps). We introduce a new dependent function type funtime whose semantics can be viewed as a cost-aware version of function extensionality. We prove a collection of lemmas for $mathbf{CATT}$, including a novel introduction rule for the new funtime type. $mathbf{CATT}$ can be simultaneously viewed as a framework for analyzing computational complexity of programs and as the beginnings of a semantic foundation for characterizing feasible mathematical proofs.
Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. While existing gradual type soundness theorems for these languages aim to show that type-based rea
soning is preserved when moving from the fully static setting to a gradual one, these theorems do not imply that correctness of type-based refactorings and optimizations is preserved. Establishing correctness of program transformations is technically difficult, and is often neglected in the metatheory of gradual languages. In this paper, we propose an axiomatic account of program equivalence in a gradual cast calculus, which we formalize in a logic we call gradual type theory (GTT). Based on Levys call-by-push-value, GTT gives an axiomatic account of both call-by-value and call-by-name gradual languages. We then prove theorems that justify optimizations and refactorings in gradually typed languages. For example, uniqueness principles for gradual type connectives show that if the $betaeta$ laws hold for a connective, then casts between that connective must be equivalent to the lazy cast semantics. Contrapositively, this shows that eager cast semantics violates the extensionality of function types. As another example, we show that gradual upcasts are pure and dually, gradual downcasts are strict. We show the consistency and applicability of our theory by proving that an 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 parametrized by the implementation of the dynamic types, and so gives a family of implementations that validate type-based optimization and the gradual guarantee.
We present gradual type theory, a logic and type theory for call-by-name gradual typing. We define the central constructions of gradual typing (the dynamic type, type casts and type error) in a novel way, by universal properties relative to new judgm
ents for gradual type and term dynamism, which were developed in blame calculi and to state the gradual guarantee theorem of gradual typing. Combined with the ordinary extensionality ($eta$) principles that type theory provides, we show that most of the standard operational behavior of casts is uniquely determined by the gradual guarantee. This provides a semantic justification for the definitions of casts, and shows that non-standard definitions of casts must violate these principles. Our type theory is the internal language of a certain class of preorder categories called equipments. We give a general construction of an equipment interpreting gradual type theory from a 2-category representing non-gradual types and programs, which is a semantic analogue of Findler and Felleisens definitions of contracts, and use it to build some concrete domain-theoretic models of gradual typing.
As quantum computers become real, it is high time we come up with effective techniques that help programmers write correct quantum programs. In classical computing, formal verification and sound static type systems prevent several classes of bugs fro
m being introduced. There is a need for similar techniques in the quantum regime. Inspired by Hoare Type Theory in the classical paradigm, we propose Quantum Hoare Types by extending the Quantum IO Monad by indexing it with pre- and post-conditions that serve as program specifications. In this paper, we introduce Quantum Hoare Type Theory (QHTT), present its syntax and typing rules, and demonstrate its effectiveness with the help of examples. QHTT has the potential to be a unified system for programming, specifying, and reasoning about quantum programs. This is a work in progress.
We show canonicity and normalization for dependent type theory with a cumulative sequence of universes and a type of Boolean. The argument follows the usual notion of reducibility, going back to Godels Dialectica interpretation and the work of Tait.
A key feature of our approach is the use of a proof relevant notion of reducibility.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
