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:

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