Problem Definition

Feature: rich set of built-in primitives (lists, algebraic data types, sets, maps)

  • well-founded

Benchmarks: interesting data structures implementations (see Chris Okasaki's book)

  • sets implemented using lists
  • relations implemented using association lists

Inference using abstraction functions, design flow

  • define concrete representation
  • define abstraction function
  • select operations of interest (insert, remove, etc.)


Collect statistics on functional programs on their structure, use them in heuristics

  • number of recursive calls small on a path
  • number of times variable is used

Machine learning over new domains (not just numbers and regular languages)


termination (invoke recursive calls on “smaller” instances), types, test-cases, statistics syntactic mesaures

design patterns, generalized fold/unfold

fail early,

Use decision procedures! learning from finite traces on small examples symmetry breaking improving efficiency through properties of domains:

  • quantifier elimination for term algebras
  • WS2S

Interaction and Hints

User-defined templates as a mechanism

  • think of this as HOL variables



lectures by Sumit

  1. logical abstract interpretation: decision procedures, abstract interpretation - 4 hours
  2. performance and bound analysis - 4.5 hours (8 hours in total)
  3. around FM in Netherlands (early November), visit EPFL if possible and give a course