48 citations · 157 across the 6 of their papers we have counts for
6 papers · 1 filter
Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification
Cameron Moy, Phúc C. Nguyen, Sam Tobin-Hochstadt +1
Gradually-typed programming languages permit the incremental addition of static types to untyped programs. To remain sound, languages insert run-time checks at the boundaries betwe…
Soft Contract Verification for Higher-Order Stateful Programs
Phuc C. Nguyen, Thomas Gilray, Sam Tobin-Hochstadt +1
Software contracts allow programmers to state rich program properties using the full expressive power of an object language. However, since they are enforced at runtime, monitoring…
Abstracting Definitional Interpreters
David Darais, Nicholas Labich, Phuc C. Nguyen +1
In this functional pearl, we examine the use of definitional interpreters as a basis for abstract interpretation of higher-order programming languages. As it turns out, definitiona…
Higher-order symbolic execution for contract verification and refutation
Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn
We present a new approach to automated reasoning about higher-order programs by endowing symbolic execution with a notion of higher-order, symbolic values. Our approach is sound an…
Relatively Complete Counterexamples for Higher-Order Programs
Phuc C. Nguyen, David Van Horn
In this paper, we study the problem of generating inputs to a higher-order program causing it to error. We first study the problem in the setting of PCF, a typed, core functional l…
Soft Contract Verification
Phuc C. Nguyen, Sam Tobin-Hochstadt, David Van Horn
Behavioral software contracts are a widely used mechanism for governing the flow of values between components. However, run-time monitoring and enforcement of contracts imposes sig…