New answers tagged type-theory
3
The rules of a type system may be given in one of several ways.
We often begin by defining a relation "term $t$ has type $A$" using rules of inference without giving any particular way of turning the rules into an algorithm. This is sometimes called the "declarative style". The declarative style is usually the easiest to understand and ...
0
I don't know much, but I am pretty sure Linear Type Theory is used to model imperative programs. For example, Adoption and focus: practical linear types for imperative programming or On linear types and imperative update. Rust, for example, is built on something related to linear types (I forget what exactly though).
It appears the more general category of ...
2
Spurred by comments in Pierre Marie's answer, I'll add some clarification on the difference between type checking and type synthesis.
Generally, type checking in a dependent type system is designed to be decidable up to normalization for fully annotated terms, that is, $\lambda x : T.t$ and $\Pi x : T. U$ for example (you need type annotations in other ...
Top 50 recent answers are included