Combining programming with theorem proving
From MaRDI portal
Publication:2936769
DOI10.1145/1086365.1086375zbMath1302.68241MaRDI QIDQ2936769
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
68N15: Theory of programming languages
Related Items
The Implicit Calculus of Constructions as a Programming Language with Dependent Types, Automated verification of shape, size and bag properties via user-defined predicates in separation logic, Type-specialized staged programming with process separation, Constructive Membership Predicates as Index Types, Type-level Computation Using Narrowing in Ωmega, Language-Based Program Verification via Expressive Types, The Nuggetizer: Abstracting Away Higher-Orderness for Program Verification, Hoare type theory, polymorphism and separation