default search action

combined dblp search
author search
venue search
publication search

ask others

CPP 2011: Kenting, Taiwan

> Home > Conferences and Workshops > CPP

Refine list

refinements active!

zoomed in on ?? of ?? records

view refined list in

export refined list as

showing all ?? records

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/2011
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/2011
Jean-Pierre Jouannaud, Zhong Shao:
Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings. Lecture Notes in Computer Science 7086, Springer 2011, ISBN 978-3-642-25378-2

APLAS/CPP Invited Talks

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Bjorner11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Bjorner11
Nikolaj S. Bjørner:
Engineering Theories with Z3. 1-2
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/OHearn11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/OHearn11
Peter W. O'Hearn:
Algebra, Logic, Locality, Concurrency. 3-4

Session 1: Logic and Types

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/DoczkalS11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/DoczkalS11
Christian Doczkal, Gert Smolka:
Constructive Formalization of Hybrid Logic with Eventualities. 5-20
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/PfenningCT11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/PfenningCT11
Frank Pfenning, Luís Caires, Bernardo Toninho:
Proof-Carrying Code in a Session-Typed Process Calculus. 21-36

Session 2: Certificates

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/StratulatD11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/StratulatD11
Sorin Stratulat, Vincent Demange:
Automated Certification of Implicit Induction Proofs. 37-53
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Miller11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Miller11
Dale Miller:
A Proposal for Broad Spectrum Proof Certificates. 54-69

Session 3: Invited Talk

- view
  - electronic edition via DOI (open access)
  - details & citations
  authority control:
- export record
  dblp key:
  - conf/cpp/Voevodsky11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Voevodsky11
Vladimir Voevodsky:
Univalent Semantics of Constructive Type Theories. 70

Session 4: Formalization

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/GenevauxNS11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/GenevauxNS11
Jean-David Génevaux, Julien Narboux, Pascal Schreck:
Formalization of Wu's Simple Method in Coq. 71-86
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/KaliszykB11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/KaliszykB11
Cezary Kaliszyk, Henk Barendregt:
Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem. 87-102
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Ridge11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Ridge11
Tom Ridge:
Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars. 103-118
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/CoquandS11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/CoquandS11
Thierry Coquand, Vincent Siles:
A Decision Procedure for Regular Expression Equivalence in Type Theory. 119-134

Session 5: Proof Assistants

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ArmandFGKTW11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ArmandFGKTW11
Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner:
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. 135-150
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BessonCP11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BessonCP11
Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie:
Modular SMT Proofs for Fast Reflexive Checking Inside Coq. 151-166
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BraibantP11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BraibantP11
Thomas Braibant, Damien Pous:
Tactics for Reasoning Modulo AC in Coq. 167-182
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BohmeFSW11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BohmeFSW11
Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, Tjark Weber:
Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. 183-198

Session 6: Teaching

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/HenzH11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/HenzH11
Martin Henz, Aquinas Hobor:
Teaching Experience: Logic and Formal Methods with Coq. 199-215
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Kahl11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Kahl11
Wolfram Kahl:
The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider's "Logical Approach to Discrete Math". 216-230

Session 7: Invited Talk

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Appel11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Appel11
Andrew W. Appel:
VeriSmall: Verified Smallfoot Shape Analysis. 231-246

Session 8: Programming Languages

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/LeiQ11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/LeiQ11
Jinjiang Lei, Zongyan Qiu:
Verification of Scalable Synchronous Queue. 247-263
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/KimR11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/KimR11
Jieung Kim, Sukyoung Ryu:
Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance. 264-279
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/CheneyU11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/CheneyU11
James Cheney, Christian Urban:
Mechanizing the Metatheory of mini-XQuery. 280-295
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BackesHT11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BackesHT11
Michael Backes, Catalin Hritcu, Thorsten Tarrach:
Automatically Verifying Typing Constraints for a Data Processing Language. 296-313

Session 9: Hardware Certification

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/NguyenM11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/NguyenM11
Thi Minh Tuyen Nguyen, Claude Marché:
Hardware-Dependent Proofs of Numerical Programs. 314-329
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Braibant11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Braibant11
Thomas Braibant:
Coquet: A Coq Library for Verifying Hardware. 330-345
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/ShiMTB11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/ShiMTB11
Xiaomu Shi, Jean-François Monin, Frédéric Tuong, Frédéric Blanqui:
First Steps towards the Certification of an ARM Simulator Using Compcert. 346-361

Session 10: Miscellaneous

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BoespflugDG11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BoespflugDG11
Mathieu Boespflug, Maxime Dénès, Benjamin Grégoire:
Full Reduction at Full Throttle. 362-377
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/CorbineauDL11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/CorbineauDL11
Pierre Corbineau, Mathilde Duclos, Yassine Lakhnech:
Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience. 378-393

Session 11: Proof Pearls

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/JiangN11
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/JiangN11
Dongchen Jiang, Tobias Nipkow:
Proof Pearl: The Marriage Theorem. 394-399

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.