Questions tagged [type-inference]
The type-inference tag has no usage guidance.
4
questions
25
votes
2answers
1k views
Context Sensitive Grammars and Types
1) What, if any, is the relationship between static typing and formal grammars?
2) In particular, would it be possible for a linear bounded automaton to check whether, say, a C++ or SML program was ...
10
votes
3answers
2k views
Type inference for imperative statements other than assignment
In my search for research papers about type systems for imperative languages, I only find solutions for a language with mutable references but without genuine imperative control structures such as ...
9
votes
1answer
431 views
In System F à la Church, can we automatize type inference for the for-all elimination?
The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by applying this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$.
Now, suppose ...
9
votes
2answers
183 views
Decidability of type inference and type checking in MLTT
In Martin-Löf's An Intuitionistic Theory of Types: Predicative Part it is proved that type checking $a \colon A$ is decidable subject to $a$ being typeable in the first place, by proving a ...
