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

User-defined templates as a mechanism

• think of this as HOL variables

• Verification and Synthesis of Data Structures, 1974
• SYNVER: A system for the automatic synthesis and verification of synchronization processes
• Toward automatic program synthesis
• A Transformation System for Developing Recursive Programs
• Narrowing and unification in functional programming —An evaluation mechanism for absolute set abstraction

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

• http://phd.epfl.ch/edic (PhD program)
• master as not necessarily tied to PhD:
  • master's in CS