Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
rml [2009/10/08 22:01]
vkuncak
rml [2010/01/29 17:43] (current)
vkuncak
Line 1: Line 1:
 ====== Rich Model Language ====== ====== Rich Model Language ======
  
-Tool chain+===== Syntax ===== 
   * lisp syntax based on Isabelle identifier names (perhaps clean-up names in Isabelle itself)   * lisp syntax based on Isabelle identifier names (perhaps clean-up names in Isabelle itself)
   * tools to provide nicer surface syntax and generate lisp syntax   * 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: Document summarizing operators of interest:
-  * http://www.cl.cam.ac.uk/​research/​hvg/​Isabelle/​dist/​Isabelle/​doc/​main.pdf+  * {{:isabellemain.pdf|What'​s in Isabelle ​Main, October 14, 2009}}
  
 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)
Line 16: Line 35:
   * no set intervals   * no set intervals
   * option types   * option types
-  * subset of list operations+  * subset of list operations