Dependent types from counterexamples
From MaRDI portal
Publication:5255067
DOI10.1145/1706299.1706315zbMath1312.68041OpenAlexW1973094460MaRDI QIDQ5255067
Publication date: 11 June 2015
Published in: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)
Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.180.9289
Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (7)
Constraint-based relational verification ⋮ Higher order symbolic execution for contract verification and refutation ⋮ Modular Verification of Higher-Order Functional Programs ⋮ Sound and complete concolic testing for higher-order functions ⋮ Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking ⋮ ICE-based refinement type discovery for higher-order functional programs ⋮ On recursion-free Horn clauses and Craig interpolation
Uses Software
This page was built for publication: Dependent types from counterexamples
