Modular Verification of Higher-Order Functional Programs

DOI10.1007/978-3-662-54434-1_31zbMath1485.68043OpenAlexW2596310084MaRDI QIDQ2988670

Naoki Kobayashi, Ryosuke Sato

Publication date: 19 May 2017

Published in: Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-54434-1_31

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• Dafny
• Haskell
• Why3
• WhyML
• MoCHi
• LiquidHaskell

Cites Work

• Unnamed Item
• Soft contract verification
• Refinement types for Haskell
• Dependent types and multi-monadic effects in F*
• Compositional and Lightweight Dependent Type Inference for ML
• Automating relatively complete verification of higher-order functional programs
• Learning refinement types
• Dafny: An Automatic Program Verifier for Functional Correctness
• Higher-Order Model Checking in Direct Style
• Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs
• Automated Assume-Guarantee Reasoning by Abstraction Refinement
• Dependent types from counterexamples
• Low-level liquid types
• Higher-order multi-parameter tree transducers and recursion schemes for program verification
• Why3 — Where Programs Meet Provers
• Verifying higher-order functional programs with pattern-matching algebraic data types

This page was built for publication: Modular Verification of Higher-Order Functional Programs