- J Strother Moore:
Reasoning about digital artifacts with ACL2. PLPV 2011: 1-2 - Meera Sridhar, Kevin W. Hamlen:
Flexible in-lined reference monitor certification: challenges and future directions. PLPV 2011: 55-60 - Gordon Stewart, Andrew W. Appel
:
Local actions for a curry-style operational semantics. PLPV 2011: 31-42 - Ranjit Jhala, Wouter Swierstra:
Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, PLPV 2011, Austin, TX, USA, January 29, 2011. ACM 2011, ISBN 978-1-4503-0487-0 [contents] - 2010
- Stephanie Balzer, Thomas R. Gross:
Modular reasoning about invariants over shared state with interposed data members. PLPV 2010: 49-56 - Jan Christiansen, Daniel Seidel, Janis Voigtländer:
Free theorems for functional logic programs. PLPV 2010: 39-48 - Matthew Danish, Hongwei Xi:
Operating system development with ATS: work in progress. PLPV 2010: 9-14 - Tomas Kalibera, Pavel Parízek, Ghaith Haddad, Gary T. Leavens, Jan Vitek:
Challenge benchmarks for verification of real-time programs. PLPV 2010: 57-62 - Stefan Monnier, David Haguenauer:
Singleton types here, singleton types there, singleton types everywhere. PLPV 2010: 1-8 - Aaron Stump, Evan Austin:
Resource typing in Guru. PLPV 2010: 27-38 - Stephanie Weirich, Chris Casinghino:
Arity-generic datatype-generic programming. PLPV 2010: 15-26 - Jean-Christophe Filliâtre, Cormac Flanagan:
Proceedings of the 4th ACM Workshop Programming Languages meets Program Verification, PLPV 2010, Madrid, Spain, January 19, 2010. ACM 2010, ISBN 978-1-60558-890-2 [contents] - 2009
- Ana Bove, Peter Dybjer, Andrés Sicard-Ramírez:
Embedding a logical theory of constructions in Agda. PLPV 2009: 59-66 - Levent Erkök, John Matthews:
Pragmatic equivalence and safety checking in Cryptol. PLPV 2009: 73-82 - Manuel Fähndrich:
Language-agnostic specification and verification: invited talk. PLPV 2009: 1-2 - Kenneth L. Knowles, Cormac Flanagan:
Compositional reasoning and decidable checking for dependent contract types. PLPV 2009: 27-38 - Daniel R. Licata, Robert Harper:
Positively dependent types. PLPV 2009: 3-14 - Max Schäfer, Torbjörn Ekman, Oege de Moor:
Challenge proposal: verification of refactorings. PLPV 2009: 67-72 - Tom Schrijvers, Louis-Julien Guillemette, Stefan Monnier:
Type invariants for Haskell. PLPV 2009: 39-48 - Aaron Stump, Morgan Deters, Adam Petcher, Todd Schiller, Timothy W. Simpson:
Verified programming in Guru. PLPV 2009: 49-58 - Noam Zeilberger:
Refinement types and computational duality. PLPV 2009: 15-26 - Thorsten Altenkirch, Todd D. Millstein:
Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009. ACM 2009, ISBN 978-1-60558-330-3 [contents] - 2007
- Thorsten Altenkirch, Conor McBride, Wouter Swierstra:
Observational equality, now! PLPV 2007: 57-68 - Jeremy E. Dawson:
Compound monads in specification languages. PLPV 2007: 3-10 - Jana Dunfield:
Refined typechecking with Stardust. PLPV 2007: 21-32 - Claude Marché:
Jessie: an intermediate language for Java and C verification. PLPV 2007: 1-2 - Adam Megacz:
A coinductive monad for prop-bounded recursion. PLPV 2007: 11-20 - Stefan Monnier:
The swiss coercion. PLPV 2007: 33-40 - Nicolas Oury:
Pattern matching coverage checking with dependent types using set approximations. PLPV 2007: 47-56 - Rui Shi:
Implementing reliable Linux device drivers in ATS. PLPV 2007: 41-46
