Rich Model Language

• 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

Classical HOL

• built in operators
• define them whenever natural, or state strong enough properties

Simple types

Parametric polymorphism

Soft typing systems on top?

Document summarizing operators of interest:

• 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