type theory
4 stories and discussions about type theory, aggregated from every source we track.
A post touring resources you can use to learn how to implement a type checker or type inference algorithm
<p>From the abstract:</p> <blockquote> <p>We consider the problem of reconciling a dependently typed functional language with imperative features such as mutable higher-order state, pointer aliasing, and non-termination. We propose Hoare Type Theory (HTT), which incorporates Hoare-style specifications into types, making it possible to statically track and enforce correct use of side effects. The main feature of HTT is the Hoare type {P}x:A{Q} specifying computations with precondition P and postcondition Q that return a result of type A. Hoare types can be nested, combined with other types, and abstracted, leading to a smooth integration with higher-order functions and type polymorphism. We further show that in the presence of type polymorphism, it becomes possible to interpret the Hoare types in the “small footprint” manner, as advocated by Separation Logic, whereby specifications tightly describe the state required by the computation. We establish that HTT is sound and compositional, in the sense that separate verifications of individual program components suffice to ensure the correctness of the composite program.</p> </blockquote> <p>Basically, they combine Hoare Triples with Dependent Types, which seems pretty interesting.</p>
A topos can be specified by the geometric theory that it classifies. Though the sequents of a theory are described formally and syntactically, its interaction with the world of sets (through set-indexed disjunctions…
The sets-as-trees interpretation of set theory in a dependent type theory with an impredicative universe of propositions validates Zermelo set theory, and it validates Replacement if the type theory has a choice or…