Table of Contents

• 1. Introduction
• 2. Refinement Logic
• 3. The Simply Typed -calculus
• 4. Branches and Recursion
• 5. Refinement Inference
• 6. Type Polymorphism
• 7. Data Types
• 8. Refinement Polymorphism
• 9. Termination
• 10. Programs as Proofs
• 11. Related Work
• 12. Conclusion
• References