Login / Signup
PLPV
2007
2010
2014
2007
2014
Keyphrases
Publications
2014
Lee Pike
,
Patrick C. Hickey
,
James Bielman
,
Trevor Elliott
,
Thomas DuBuisson
,
John Launchbury
Programming languages for high-assurance autonomous vehicles: extended abstract.
PLPV
(2014)
Wolfgang Jeltsch
An abstract categorical semantics for functional reactive programming with processes.
PLPV
(2014)
Ranjit Jhala
Refinement types for Haskell.
PLPV
(2014)
Aaron Stump
The recursive polarized dual calculus.
PLPV
(2014)
Martin Clochard
,
Claude Marché
,
Andrei Paskevich
Verified programs with binders.
PLPV
(2014)
Proceedings of the 2014 ACM SIGPLAN Workshop on Programming Languages meets Program Verification, PLPV 2014, January 21, 2014, San Diego, California, USA, Co-located with POPL '14
PLPV
(2014)
Noriko Hirota
,
Kenichi Asai
Formalizing a correctness property of a type-directed partial evaluator.
PLPV
(2014)
Filipe Militão
,
Jonathan Aldrich
,
Luís Caires
Substructural typestates.
PLPV
(2014)
2013
Wolfgang Jeltsch
Temporal logic with "Until", functional reactive programming with processes, and concrete process categories.
PLPV
(2013)
Proceedings of the 7th Workshop on Programming languages meets program verification, PLPV 2013, Rome, Italy, January 22, 2013
PLPV
(2013)
Norman Danner
,
Jennifer Paykin
,
James S. Royer
A static cost analysis for a higher-order language.
PLPV
(2013)
Francisco Ferreira
,
Stefan Monnier
,
Brigitte Pientka
Compiling contextual objects: bringing higher-order abstract syntax to programmers.
PLPV
(2013)
Reynald Affeldt
,
Nicolas Marti
Towards formal verification of TLS network packet processing written in C.
PLPV
(2013)
Christopher Schwaab
,
Jeremy G. Siek
Modular type-safety proofs in Agda.
PLPV
(2013)
Edwin C. Brady
Idris: general purpose programming with dependent types.
PLPV
(2013)
Alan Jeffrey
Causality for free!: parametricity implies causality for functional reactive programs.
PLPV
(2013)
Clara Bertolissi
,
Worachet Uttha
Automated analysis of rule-based access control policies.
PLPV
(2013)
2012
Alan Jeffrey
LTL types FRP: linear-time temporal logic propositions as types, proofs as functional reactive programs.
PLPV
(2012)
Peter-Michael Osera
,
Vilhelm Sjöberg
,
Steve Zdancewic
Dependent interoperability.
PLPV
(2012)
Reynald Affeldt
,
David Nowak
,
Yutaka Oiwa
Formal network packet processing with minimal fuss: invertible syntax descriptions at work.
PLPV
(2012)
Afshin Amighi
,
Stefan Blom
,
Marieke Huisman
,
Marina Zaharieva-Stojanovski
The VerCors project: setting up basecamp.
PLPV
(2012)
Manuel Gesell
,
Klaus Schneider
A hoare calculus for the verification of synchronous languages.
PLPV
(2012)
Garrin Kimmell
,
Aaron Stump
,
Harley D. Eades III
,
Peng Fu
,
Tim Sheard
,
Stephanie Weirich
,
Chris Casinghino
,
Vilhelm Sjöberg
,
Nathan Collins
,
Ki Yung Ahn
Equational reasoning about programs with general recursion and call-by-value semantics.
PLPV
(2012)
Vladimir Komendantsky
Reflexive toolbox for regular expression matching: verification of functional programs in Coq+Ssreflect.
PLPV
(2012)
Benjamin C. Pierce
Verification challenges of pervasive information flow.
PLPV
(2012)
Proceedings of the sixth workshop on Programming Languages meets Program Verification, PLPV 2012, Philadelphia, PA, USA, January 24, 2012
PLPV
(2012)
2011
Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, PLPV 2011, Austin, TX, USA, January 29, 2011
PLPV
(2011)
Meera Sridhar
,
Kevin W. Hamlen
Flexible in-lined reference monitor certification: challenges and future directions.
PLPV
(2011)
Derek Bronish
,
Hampton Smith
Robust, generic, modularly-verified map: a software verification challenge problem.
PLPV
(2011)
Shuvendu K. Lahiri
,
Shaz Qadeer
,
David Walker
Linear maps.
PLPV
(2011)
Edwin C. Brady
IDRIS ---: systems programming meets full dependent types.
PLPV
(2011)
Johannes Borgström
,
Juan Chen
,
Nikhil Swamy
Verifying stateful programs with substructural state and hoare types.
PLPV
(2011)
Gordon Stewart
,
Andrew W. Appel
Local actions for a curry-style operational semantics.
PLPV
(2011)
J Strother Moore
Reasoning about digital artifacts with ACL2.
PLPV
(2011)
2010
Aaron Stump
,
Evan Austin
Resource typing in Guru.
PLPV
(2010)
Stephanie Balzer
,
Thomas R. Gross
Modular reasoning about invariants over shared state with interposed data members.
PLPV
(2010)
Stephanie Weirich
,
Chris Casinghino
Arity-generic datatype-generic programming.
PLPV
(2010)
Jan Christiansen
,
Daniel Seidel
,
Janis Voigtländer
Free theorems for functional logic programs.
PLPV
(2010)
Stefan Monnier
,
David Haguenauer
Singleton types here, singleton types there, singleton types everywhere.
PLPV
(2010)
Proceedings of the 4th ACM Workshop Programming Languages meets Program Verification, PLPV 2010, Madrid, Spain, January 19, 2010
PLPV
(2010)
Matthew Danish
,
Hongwei Xi
Operating system development with ATS: work in progress.
PLPV
(2010)
Tomas Kalibera
,
Pavel Parízek
,
Ghaith Haddad
,
Gary T. Leavens
,
Jan Vitek
Challenge benchmarks for verification of real-time programs.
PLPV
(2010)
2009
Manuel Fähndrich
Language-agnostic specification and verification: invited talk.
PLPV
(2009)
Ana Bove
,
Peter Dybjer
,
Andrés Sicard-Ramírez
Embedding a logical theory of constructions in Agda.
PLPV
(2009)
Kenneth Knowles
,
Cormac Flanagan
Compositional reasoning and decidable checking for dependent contract types.
PLPV
(2009)
Levent Erkök
,
John Matthews
Pragmatic equivalence and safety checking in Cryptol.
PLPV
(2009)
Aaron Stump
,
Morgan Deters
,
Adam Petcher
,
Todd Schiller
,
Timothy W. Simpson
Verified programming in Guru.
PLPV
(2009)
Noam Zeilberger
Refinement types and computational duality.
PLPV
(2009)
Max Schäfer
,
Torbjörn Ekman
,
Oege de Moor
Challenge proposal: verification of refactorings.
PLPV
(2009)
Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009
PLPV
(2009)