## 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 | 9554 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 hours 56 min ago

6 hours 25 sec ago

6 hours 42 sec ago

6 hours 4 min ago

7 hours 15 min ago

7 hours 20 min ago

8 hours 17 min ago

8 hours 39 min ago

8 hours 41 min ago

9 hours 8 min ago