Combining programming with theorem proving

DOI10.1145/1086365.1086375zbMath1302.68241OpenAlexW2134801812MaRDI QIDQ2936769

Hongwei Xi, Chiyan Chen

Publication date: 6 January 2015

Published in: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1086365.1086375

zbMATH Keywords

theorem provingdependent typesapplied type systemATSproof erasure

Mathematics Subject Classification ID

Related Items (8)

Type-specialized staged programming with process separation ⋮ The Nuggetizer: Abstracting Away Higher-Orderness for Program Verification ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ Hoare type theory, polymorphism and separation ⋮ The Implicit Calculus of Constructions as a Programming Language with Dependent Types ⋮ Constructive Membership Predicates as Index Types ⋮ Type-level Computation Using Narrowing in Ωmega ⋮ Language-Based Program Verification via Expressive Types

This page was built for publication: Combining programming with theorem proving