| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Lee Pike, Patrick C. Hickey, James Bielman, Trevor Elliott, Thomas DuBuisson, John Launchbury |
Programming languages for high-assurance autonomous vehicles: extended abstract.  |
PLPV  |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Noriko Hirota, Kenichi Asai |
Formalizing a correctness property of a type-directed partial evaluator. |
PLPV |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Wolfgang Jeltsch |
An abstract categorical semantics for functional reactive programming with processes. |
PLPV |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Nils Anders Danielsson, Bart Jacobs 0002 (eds.) |
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 |
DBLP BibTeX RDF |
|
| 1 | Filipe Militão, Jonathan Aldrich, Luís Caires |
Substructural typestates. |
PLPV |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Ranjit Jhala |
Refinement types for Haskell. |
PLPV |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Martin Clochard, Claude Marché, Andrei Paskevich |
Verified programs with binders. |
PLPV |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Aaron Stump |
The recursive polarized dual calculus. |
PLPV |
2014 |
DBLP DOI BibTeX RDF |
|
| 1 | Wolfgang Jeltsch |
Temporal logic with "Until", functional reactive programming with processes, and concrete process categories. |
PLPV |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Edwin C. Brady |
Idris: general purpose programming with dependent types. |
PLPV |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Reynald Affeldt, Nicolas Marti |
Towards formal verification of TLS network packet processing written in C. |
PLPV |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Clara Bertolissi, Worachet Uttha |
Automated analysis of rule-based access control policies. |
PLPV |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthew Might, David Van Horn, Andreas Abel 0001, Tim Sheard (eds.) |
Proceedings of the 7th Workshop on Programming languages meets program verification, PLPV 2013, Rome, Italy, January 22, 2013 |
PLPV |
2013 |
DBLP BibTeX RDF |
|
| 1 | Norman Danner, Jennifer Paykin, James S. Royer |
A static cost analysis for a higher-order language. |
PLPV |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Francisco Ferreira 0001, Stefan Monnier, Brigitte Pientka |
Compiling contextual objects: bringing higher-order abstract syntax to programmers. |
PLPV |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Christopher Schwaab, Jeremy G. Siek |
Modular type-safety proofs in Agda. |
PLPV |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Alan Jeffrey |
Causality for free!: parametricity implies causality for functional reactive programs. |
PLPV |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Garrin Kimmell, Aaron Stump, Harley D. Eades III, Peng Fu 0001, 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Reynald Affeldt, David Nowak, Yutaka Oiwa |
Formal network packet processing with minimal fuss: invertible syntax descriptions at work. |
PLPV |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter-Michael Osera, Vilhelm Sjöberg, Steve Zdancewic |
Dependent interoperability. |
PLPV |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Benjamin C. Pierce |
Verification challenges of pervasive information flow. |
PLPV |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Alan Jeffrey |
LTL types FRP: linear-time temporal logic propositions as types, proofs as functional reactive programs. |
PLPV |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Manuel Gesell, Klaus Schneider 0001 |
A hoare calculus for the verification of synchronous languages. |
PLPV |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Koen Claessen, Nikhil Swamy (eds.) |
Proceedings of the sixth workshop on Programming Languages meets Program Verification, PLPV 2012, Philadelphia, PA, USA, January 24, 2012 |
PLPV |
2012 |
DBLP BibTeX RDF |
|
| 1 | Afshin Amighi, Stefan Blom, Marieke Huisman, Marina Zaharieva-Stojanovski |
The VerCors project: setting up basecamp. |
PLPV |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Vladimir Komendantsky |
Reflexive toolbox for regular expression matching: verification of functional programs in Coq+Ssreflect. |
PLPV |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Meera Sridhar, Kevin W. Hamlen |
Flexible in-lined reference monitor certification: challenges and future directions. |
PLPV |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Ranjit Jhala, Wouter Swierstra (eds.) |
Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, PLPV 2011, Austin, TX, USA, January 29, 2011 |
PLPV |
2011 |
DBLP BibTeX RDF |
|
| 1 | Edwin C. Brady |
IDRIS ---: systems programming meets full dependent types. |
PLPV |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | J Strother Moore |
Reasoning about digital artifacts with ACL2. |
PLPV |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Shuvendu K. Lahiri, Shaz Qadeer, David Walker 0001 |
Linear maps. |
PLPV |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Derek Bronish, Hampton Smith |
Robust, generic, modularly-verified map: a software verification challenge problem. |
PLPV |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Johannes Borgström, Juan Chen 0002, Nikhil Swamy |
Verifying stateful programs with substructural state and hoare types. |
PLPV |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Gordon Stewart 0001, Andrew W. Appel |
Local actions for a curry-style operational semantics. |
PLPV |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Tomas Kalibera, Pavel Parízek, Ghaith Haddad, Gary T. Leavens, Jan Vitek |
Challenge benchmarks for verification of real-time programs. |
PLPV |
2010 |
DBLP DOI BibTeX RDF |
java, verification, real-time |
| 1 | Stephanie Balzer, Thomas R. Gross |
Modular reasoning about invariants over shared state with interposed data members. |
PLPV |
2010 |
DBLP DOI BibTeX RDF |
ownership type systems, invariants |
| 1 | Aaron Stump, Evan Austin |
Resource typing in Guru. |
PLPV |
2010 |
DBLP DOI BibTeX RDF |
dependently typed programming, resource types |
| 1 | Jan Christiansen, Daniel Seidel, Janis Voigtländer |
Free theorems for functional logic programs. |
PLPV |
2010 |
DBLP DOI BibTeX RDF |
haskell, relational parametricity, curry |
| 1 | Stefan Monnier, David Haguenauer |
Singleton types here, singleton types there, singleton types everywhere. |
PLPV |
2010 |
DBLP DOI BibTeX RDF |
dependent types, certified compilation, singleton types |
| 1 | Stephanie Weirich, Chris Casinghino |
Arity-generic datatype-generic programming. |
PLPV |
2010 |
DBLP DOI BibTeX RDF |
agda, arity-generic programming, generic haskell, dependent types |
| 1 | Matthew Danish, Hongwei Xi |
Operating system development with ATS: work in progress. |
PLPV |
2010 |
DBLP DOI BibTeX RDF |
linear types, operating systems, dependent types |
| 1 | Jean-Christophe Filliâtre, Cormac Flanagan (eds.) |
Proceedings of the 4th ACM Workshop Programming Languages meets Program Verification, PLPV 2010, Madrid, Spain, January 19, 2010 |
PLPV |
2010 |
DBLP BibTeX RDF |
|
| 1 | Ana Bove, Peter Dybjer, Andrés Sicard-Ramírez |
Embedding a logical theory of constructions in Agda. |
PLPV |
2009 |
DBLP DOI BibTeX RDF |
general recursion, logical theory of constructions, type theory |
| 1 | Kenneth L. Knowles, Cormac Flanagan |
Compositional reasoning and decidable checking for dependent contract types. |
PLPV |
2009 |
DBLP DOI BibTeX RDF |
refinement types, abstraction, dependent types, compositional reasoning |
| 1 | Aaron Stump, Morgan Deters, Adam Petcher, Todd Schiller, Timothy W. Simpson |
Verified programming in Guru. |
PLPV |
2009 |
DBLP DOI BibTeX RDF |
dependently typed programming, language-based verification, operational type theory |
| 1 | Thorsten Altenkirch, Todd D. Millstein (eds.) |
Proceedings of the 3rd ACM Workshop Programming Languages meets Program Verification, PLPV 2009, Savannah, GA, USA, January 20, 2009 |
PLPV |
2009 |
DBLP BibTeX RDF |
|
| 1 | Daniel R. Licata, Robert Harper 0001 |
Positively dependent types. |
PLPV |
2009 |
DBLP DOI BibTeX RDF |
agda, dependent types, polarity |
| 1 | Tom Schrijvers, Louis-Julien Guillemette, Stefan Monnier |
Type invariants for Haskell. |
PLPV |
2009 |
DBLP DOI BibTeX RDF |
type families, type functions, haskell, type checking |
| 1 | Manuel Fähndrich |
Language-agnostic specification and verification: invited talk. |
PLPV |
2009 |
DBLP DOI BibTeX RDF |
specifications, static analysis, abstract interpretation, contracts, net |
| 1 | Levent Erkök, John Matthews |
Pragmatic equivalence and safety checking in Cryptol. |
PLPV |
2009 |
DBLP DOI BibTeX RDF |
sat/smt solving, size polymorphism, formal methods, cryptography, theorem proving, equivalence checking |
| 1 | Max Schäfer, Torbjörn Ekman 0001, Oege de Moor |
Challenge proposal: verification of refactorings. |
PLPV |
2009 |
DBLP DOI BibTeX RDF |
refactoring, proof assistants, mechanical verification |
| 1 | Noam Zeilberger |
Refinement types and computational duality. |
PLPV |
2009 |
DBLP DOI BibTeX RDF |
duality, effects, intersection types, focusing, union types |
| 1 | Claude Marché |
Jessie: an intermediate language for Java and C verification. |
PLPV |
2007 |
DBLP DOI BibTeX RDF |
behavioral properties, verification conditions generator, verification |
| 1 | Thorsten Altenkirch, Conor McBride, Wouter Swierstra |
Observational equality, now! |
PLPV |
2007 |
DBLP DOI BibTeX RDF |
type theory, equality |
| 1 | Adam Megacz |
A coinductive monad for prop-bounded recursion. |
PLPV |
2007 |
DBLP DOI BibTeX RDF |
coinductive types, type theory |
| 1 | Stefan Monnier |
The swiss coercion. |
PLPV |
2007 |
DBLP DOI BibTeX RDF |
type based security, formal methods, compilation, coercions |
| 1 | Aaron Stump, Hongwei Xi (eds.) |
Proceedings of the ACM Workshop Programming Languages meets Program Verification, PLPV 2007, Freiburg, Germany, October 5, 2007 |
PLPV |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Jana Dunfield |
Refined typechecking with Stardust. |
PLPV |
2007 |
DBLP DOI BibTeX RDF |
type refinements, dependent types, intersection types, union types |
| 1 | Jeremy E. Dawson |
Compound monads in specification languages. |
PLPV |
2007 |
DBLP DOI BibTeX RDF |
angelic choice, compound monads, demonic choice, distributive law for monads, extended substitutions, specification languages, generalised substitutions |
| 1 | Rui Shi |
Implementing reliable Linux device drivers in ATS. |
PLPV |
2007 |
DBLP DOI BibTeX RDF |
applied type system, device driver programming, ATS |
| 1 | Nicolas Oury |
Pattern matching coverage checking with dependent types using set approximations. |
PLPV |
2007 |
DBLP DOI BibTeX RDF |
coverage checking, set approximation, pattern matching |
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license