Language-Based Program Verification via Expressive Types
From MaRDI portal
Publication:2866340
DOI10.1016/j.entcs.2006.10.041zbMath1277.68060OpenAlexW2018617042MaRDI QIDQ2866340
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
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
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