ترغب بنشر مسار تعليمي؟ اضغط هنا

An Equational Logical Framework for Type Theories

125   0   0.0 ( 0 )
 نشر من قبل Robert Harper
 تاريخ النشر 2021
  مجال البحث الهندسة المعلوماتية
والبحث باللغة English
 تأليف Robert Harper




اسأل ChatGPT حول البحث

A wide range of intuitionistic type theories may be presented as equational theories within a logical framework. This method was formulated by Per Martin-L{o}f in the mid-1980s and further developed by Uemura, who used it to prove an initiality result for a class of models. Herein is presented a logical framework for type theories that includes an extensional equality type so that a type theory may be given by a signature of constants. The framework is illustrated by a number of examples of type-theoretic concepts, including identity and equality types, and a hierarchy of universes.



قيم البحث

اقرأ أيضاً

179 - Jan A. Bergstra 2016
An equational axiomatisation of probability functions for one-dimensional event spaces in the language of signed meadows is expanded with conditional values. Conditional values constitute a so-called signed vector meadow. In the presence of a probabi lity function, equational axioms are provided for expected value, variance, covariance, and correlation squared, each defined for conditional values. Finite support summation is introduced as a binding operator on meadows which simplifies formulating requirements on probability mass functions with finite support. Conditional values are related to probability mass functions and to random variables. The definitions are reconsidered in a finite dimensional setting.
Cubical type theory provides a constructive justification of homotopy type theory. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on the type involving several non-canonical cho ices. We present in this article two canonicity results, both proved by a sconing argument: a homotopy canonicity result, every natural number is path equal to a numeral, even if we take away the equations defining the lifting operation on the type structure, and a canonicity result, which uses these equations in a crucial way. Both proofs are done internally in a presheaf model.
237 - Derek Dreyer 2011
Appel and McAllesters step-indexed logical relations have proven to be a simple and effective technique for reasoning about programs in languages with semantically interesting types, such as general recursive types and general reference types. Howeve r, proofs using step-indexed models typically involve tedious, error-prone, and proof-obscuring step-index arithmetic, so it is important to develop clean, high-level, equational proof principles that avoid mention of step indices. In this paper, we show how to reason about binary step-indexed logical relations in an abstract and elegant way. Specifically, we define a logic LSLR, which is inspired by Plotkin and Abadis logic for parametricity, but also supports recursively defined relations by means of the modal later operator from Appel, Melli`es, Richards, and Vouillons very modal model paper. We encode in LSLR a logical relation for reasoning relationally about programs in call-by-value System F extended with general recursive types. Using this logical relation, we derive a set of useful rules with which we can prove contextual equivalence and approximation results without counting steps.
128 - Christian Herrmann 2018
We study the computational complexity of satisfiability problems for classes of simple finite height (ortho)complemented modular lattices $L$. For single finite $L$, these problems are shown tobe $mc{NP}$-complete; for $L$ of height at least $3$, equ ivalent to a feasibility problem for the division ring associated with $L$. Moreover, it is shown that the equational theory of the class of subspace ortholattices as well as endomorphism *-rings (with pseudo-inversion) of finite dimensional Hilbert spaces is complete for the complement of the Boolean part of the nondeterministic Blum-Shub-Smale model of real computation without constants. This results extends to the category of finite dimensional Hilbert spaces, enriched by pseudo-inversion.
69 - Olivier Finkel 2018
We prove that $omega$-regular languages accepted by Buchi or Muller automata satisfy an effective automata-theoretic version of the Baire property. Then we use this result to obtain a new effective property of rational functions over infinite words w hich are realized by finite state Buchi transducers: for each such function $F: Sigma^omega rightarrow Gamma^omega$, one can construct a deterministic Buchi automaton $mathcal{A}$ accepting a dense ${bf Pi}^0_2$-subset of $Sigma^omega$ such that the restriction of $F$ to $L(mathcal{A})$ is continuous.
التعليقات
جاري جلب التعليقات جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
mircosoft-partner

هل ترغب بارسال اشعارات عن اخر التحديثات في شمرا-اكاديميا