## 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 | 9341 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

7 hours 47 min ago

9 hours 55 min ago

17 hours 10 min ago

22 hours 9 min ago

22 hours 20 min ago

1 day 25 min ago

1 day 7 hours ago

1 day 8 hours ago

1 day 11 hours ago

1 day 12 hours ago