## User login## Navigation |
## Type Theory## Eliminating Array Bound Checking through Non-dependent types
Oleg posted this pertinent message on the Haskell mailing list. It's always nice to see cool examples such as this.
Having saiod that, I must also say that I agree with Conor McBride who wrote that Making type systems more expressive is a worthy goal. You want them to remain decidable (i.e., static), of course. Can we at least agree on that? ;-) ## TyPiCal: Type-based static analyzer for the Pi-CalculusTyPiCal is a type-based static analyzer for the pi-calculus. The current version of TyPiCal provides four kinds of program analyses or program transformations: lock-freedom analysis, deadlock-freedom analysis, useless-code elimination, and information flow analysis. Type system is an ordinary type system extended so that channel types carry precise information about how each channel is used. This allows a type inferencer to obtain information about the behavior of a process. ## Wobbly types## Wobbly types: type inference for generalised algebraic data types
By Bryn Keller at 2004-07-19 16:19 | Functional | Type Theory | 7 comments | other blogs | 9720 reads
## Constraint-Based Type Inference for Guarded Algebraic Data Types
Constraint-Based Type Inference for Guarded Algebraic Data Types. Vincent Simonet and Francois Pottier.
Seems rather interesting. |
## Browse archives## Active forum topics |

## Recent comments

4 days 21 hours ago

5 days 49 min ago

5 days 1 hour ago

1 week 1 day ago

1 week 2 days ago

1 week 3 days ago

1 week 3 days ago

1 week 3 days ago

1 week 4 days ago

1 week 4 days ago