Language-Based Program Verification via Expressive Types

DOI10.1016/j.entcs.2006.10.041zbMath1277.68060OpenAlexW2018617042MaRDI QIDQ2866340

Martin Sulzmann, Răzvan Voicu

Publication date: 13 December 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2006.10.041

zbMATH Keywords

type inferenceresource usage verificationtype error reportingverifying sortedness

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Coq
• Haskell
• GHC
• Twelf
• Cayenne

Cites Work

• Combining programming with theorem proving
• Associated type synonyms
• A language-based approach to functionally correct imperative programming
• Guarded recursive datatype constructors
• A Framework for Extended Algebraic Data Types
• Constraint Handling Rules
• Enforcing trace properties by program transformation
• A type system for expressive security policies
• Dependent ML An approach to practical programming with dependent types
• Cayenne—a language with dependent types
• Programming Languages and Systems
• Programming Languages and Systems
• Unnamed Item
• Unnamed Item
• Unnamed Item