# Questions tagged [type-theory]

formal systems to specify properties of objects

312 questions
283 views

### What terms type systems exclude?

I understand type systems like the simply typed lambda calculus, system F and the calculus of constructions include a different subset of all lambda terms. But what, precisely, are the terms each of ...
1k views

### Daily Applications of Type Theory

I want to understand type theory but I have to know first how I can apply it. Could there be more non-obvious applications of type theory aside from in type systems in programming? Could there be ...
575 views

### In the Curry-Howard isomorphism as applied to Hindley-Milner types, what proposition corresponds to a -> [a]?

(Using Haskell syntax, since the question is inspired by Haskell, but it applies to general Hindley-Milner polymorphic type systems, such as SML or Elm). If I have a type signature ...
243 views

### What is the Curry-Howard analogue for linear logics?

As defined by Wikipedia, (The Curry-Howard correspondence) is a generalization of a syntactic analogy between systems of formal logic and computational calculi that was first discovered by the ...
44 views

### Can big-step semantics express evaluation order?

Can you express evaluation order using big-step semantics? For example, in a simple language consisting of only if t then t else t and ...
277 views

### Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program?

Chapter 7 of The Haskell Road to Logic Math and Programming discusses induction and recursion. Haskell is strongly typed and we can define the natural numbers ...
3k views

### Which research languages have a stronger typesystem than Haskell and why?

Here I read that: Haskell definitely does not have the most advanced type system (not even close if you count research languages) but out of all languages that are actually used in production ...
74 views

129 views

### Are there models of type theory that allow the real numbers to be a type?

Do there exist models of type theory that allow types to contain an uncountable number of inhabitants? Traditionally type theory seems to be swirled in with computable programs as constructive proofs ...
114 views

### Unrolling multi-variable mu (μ) expressions in type theory

Unrolling an iso-recursive μ-type expression such as, say, one isomorphic to natural numbers: μα.1+α using ...