Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
rml [2010/01/29 16:45] vkuncak |
rml [2010/01/29 17:43] (current) vkuncak |
||
|---|---|---|---|
| Line 13: | Line 13: | ||
| * built in operators | * built in operators | ||
| * define them whenever natural, or state strong enough properties | * define them whenever natural, or state strong enough properties | ||
| + | |||
| + | ===== Type System ===== | ||
| + | |||
| + | Simple types | ||
| + | |||
| + | Parametric polymorphism | ||
| + | |||
| + | Soft typing systems on top? | ||
| ===== Starting Points ===== | ===== Starting Points ===== | ||
| Line 21: | Line 29: | ||
| Some differences: | Some differences: | ||
| * separate operators for + on integers, reals | * separate operators for + on integers, reals | ||
| - | * no 'nat' for now, indexing lists gives unknown value | + | * no 'nat' for now, indexing lists gives unknown value for negative |
| * a 'finite' predicate, no separate type | * a 'finite' predicate, no separate type | ||
| * introduce a type for SMT-LIB 2.0 (same problem for maps) | * introduce a type for SMT-LIB 2.0 (same problem for maps) | ||