default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDCPP 2011: Kenting, Taiwan
- 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
- Nikolaj S. Bjørner:
Engineering Theories with Z3. 1-2 - Peter W. O'Hearn:
Algebra, Logic, Locality, Concurrency. 3-4
Session 1: Logic and Types
- Christian Doczkal, Gert Smolka:
Constructive Formalization of Hybrid Logic with Eventualities. 5-20 - Frank Pfenning, Luís Caires, Bernardo Toninho:
Proof-Carrying Code in a Session-Typed Process Calculus. 21-36
Session 2: Certificates
- Sorin Stratulat, Vincent Demange:
Automated Certification of Implicit Induction Proofs. 37-53 - Dale Miller:
A Proposal for Broad Spectrum Proof Certificates. 54-69
Session 3: Invited Talk
- Vladimir Voevodsky:
Univalent Semantics of Constructive Type Theories. 70
Session 4: Formalization
- Jean-David Génevaux, Julien Narboux, Pascal Schreck:
Formalization of Wu's Simple Method in Coq. 71-86 - Cezary Kaliszyk, Henk Barendregt:
Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem. 87-102 - Tom Ridge:
Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars. 103-118 - Thierry Coquand, Vincent Siles:
A Decision Procedure for Regular Expression Equivalence in Type Theory. 119-134
Session 5: Proof Assistants
- 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 - Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie:
Modular SMT Proofs for Fast Reflexive Checking Inside Coq. 151-166 - Thomas Braibant, Damien Pous:
Tactics for Reasoning Modulo AC in Coq. 167-182 - 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
- Martin Henz, Aquinas Hobor:
Teaching Experience: Logic and Formal Methods with Coq. 199-215 - 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
- Andrew W. Appel:
VeriSmall: Verified Smallfoot Shape Analysis. 231-246
Session 8: Programming Languages
- Jinjiang Lei, Zongyan Qiu:
Verification of Scalable Synchronous Queue. 247-263 - Jieung Kim, Sukyoung Ryu:
Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance. 264-279 - James Cheney, Christian Urban:
Mechanizing the Metatheory of mini-XQuery. 280-295 - Michael Backes, Catalin Hritcu, Thorsten Tarrach:
Automatically Verifying Typing Constraints for a Data Processing Language. 296-313
Session 9: Hardware Certification
- Thi Minh Tuyen Nguyen, Claude Marché:
Hardware-Dependent Proofs of Numerical Programs. 314-329 - Thomas Braibant:
Coquet: A Coq Library for Verifying Hardware. 330-345 - 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
- Mathieu Boespflug, Maxime Dénès, Benjamin Grégoire:
Full Reduction at Full Throttle. 362-377 - 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
- 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.
last updated on 2025-10-30 00:51 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
