Regular Language Type Inference with Term Rewriting
summary
Claims fully automatic inference of regular-language types for higher-order, tree-processing programs by modeling semantics as term rewriting and types as tree automata. It learns invariants with a counterexample-guided loop using tree automata completion plus SMT solving, is regularly-complete and complete in refutation, and ships as an OCaml extension to Timbuk. Evaluation on 80+ benchmarks solves 16% more problems than prior Timbuk and cuts worst-case memory to under 40 MB.
AI-written summary · about
chapters (10)
- 0:00Intro
- 0:35Fully Automatic Verification of Higher-Order Functional Programs processing Algebraic Datatypes
- 1:46Current verification techniques vs. regular properties Techniques classification
- 5:21From Functional Programs to Terms Rewriting Systems A rewriting systems defines a set of rewriting rules between patterns encoding the program's semantics
- 6:05Regular Languages and Tree Automata A tree automaton is a rewriting system defining a regular set of terms.
- 7:07Verification Settings The initial problem becomes a rewriting problem, then a type checking problem: User input
- 8:25Typing Algorithm
- 9:33Type inference Input: a TRS R, a symbol f, a target output (regular language) type 0.
- 10:37Regular Invariant Learning SMT-based CEGAR procedure on Tree Automata 1. Experiment 2. Observation 3. Hypothesis
- 13:29Experiments & Conclusion Implementation in Timbuk 4, tested on 80+ problems, compared with Timbuk 3
related talks
56mOn Type-Based Techniques for Program Manipulation
29mType Checking with Rewriting Rules
19mType Inference Logics
17mFrom Traces to Program Incorrectness: A Type-Theoretic Approach
18mDeveloping a Dependently Typed Language with Runtime Proof Search
14mA Limited Case for Reification by Type Inference
12mToward Grammar Inference via Refinement Types (Extended Abstract)
23mAnswer Refinement Modification: Refinement Type System for Algebraic Effects and...