Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Fri 28 Sep 2018 13:30 - 13:55 at New York Central - Session 2

ML originated as the metalanguage for constructing proofs in the LCF theorem prover. Due to its many virtues, it became a rôle model for object-level languages as well, inspiring an entire family of strict functional programming languages.

A member of this family is F*, a verification-oriented dialect of ML including dependent types and a monadic effect system, the combination of which allows to express arbitrarily complex properties of (effectful!) programs within the type system itself. To prove these properties, F* relies on querying an SMT solver (usually Z3). For properties in well-supported SMT theories (e.g. linear arithmetic or uninterpreted functions) this approach works very well, allowing programmers to verify programs with relative ease. However, for poorly-supported theories (e.g. non-linear arithmetic), the SMT solver might require a prohibitive amount of resources or be wildly inpredictable. Furthermore, these rotten apples spoil the barrel, since combining even a basic proveable fact from a poorly-supported theory with a well-supported one might stump the solver.

Motivated by these issues, we have recently extended F* with a tactics engine, which allows to attack proof obligations with user-defined procedures. Tactics are written in Meta-F* , which is simply the set of those F* programs of a particular Tac effect, defined within the existing type-and-effect system. As such, they readily interoperate with the rest of language and can themselves be verified (to a degree). Using tactics allows the programmer to massage proof obligations before querying the SMT solver (possibly simplifying them into the well-supported fragments) or even solving them completely.

Here, we present an overview of the tactics and metaprogramming engine of F*, focusing on the design of the metalanguage and its execution models. In addition, we discuss the benefits of tactics and metaprogramming in F* through some idiomatic case studies.

ML 2018 Meta-F* paper (paper.pdf)342KiB

Fri 28 Sep
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

13:30 - 15:10: Session 2ML at New York Central
13:30 - 13:55
ML as a Tactic Language, Again
Guido MartínezCIFASIS-CONICET, Argentina, Danel AhmanUniversity of Ljubljana, Victor Dumitrescu, Nick GiannarakisPrinceton University, Chris HawblitzelMicrosoft Research, Cătălin HriţcuInria Paris, Monal Narasimhamurthy, Zoe ParaskevopoulouPrinceton University, Clément Pit-ClaudelMIT CSAIL, Jonathan ProtzenkoMicrosoft Research, Redmond, Tahina RamananandroMicrosoft Research, n.n., Aseem RastogiMicrosoft Research, Nikhil SwamyMicrosoft Research
File Attached
13:55 - 14:20
Design and verification of functional proof checkers
14:20 - 14:45
14:45 - 15:10
Generic Programming with Combinators and Objects