Differences
This shows you the differences between two versions of the page.
| Next revision | Previous revision | ||
|
rml [2009/10/08 21:41] vkuncak created |
rml [2010/01/29 17:43] (current) vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Rich Model Language ====== | ====== Rich Model Language ====== | ||
| - | * http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/main.pdf | + | ===== Syntax ===== |
| + | |||
| + | * lisp syntax based on Isabelle identifier names (perhaps clean-up names in Isabelle itself) | ||
| + | * tools to provide nicer surface syntax and generate lisp syntax | ||
| + | * we have a candidate using LR(1) parser (CUP) | ||
| + | * an earlier version: [[Vepar Grammar]] | ||
| + | |||
| + | ===== Semantics ===== | ||
| + | |||
| + | Classical HOL | ||
| + | * built in operators | ||
| + | * define them whenever natural, or state strong enough properties | ||
| + | |||
| + | ===== Type System ===== | ||
| + | |||
| + | Simple types | ||
| + | |||
| + | Parametric polymorphism | ||
| + | |||
| + | Soft typing systems on top? | ||
| + | |||
| + | ===== Starting Points ===== | ||
| + | |||
| + | Document summarizing operators of interest: | ||
| + | * {{:isabellemain.pdf|What's in Isabelle Main, October 14, 2009}} | ||
| + | |||
| + | Some differences: | ||
| + | * separate operators for + on integers, reals | ||
| + | * no 'nat' for now, indexing lists gives unknown value for negative | ||
| + | * a 'finite' predicate, no separate type | ||
| + | * introduce a type for SMT-LIB 2.0 (same problem for maps) | ||
| + | * finiteness inference | ||
| + | * no set intervals | ||
| + | * option types | ||
| + | * a subset of list operations | ||