CPP 2011: Kenting, Taiwan

APLAS/CPP Invited Talks

• Nikolaj 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
  

Last update Thu May 24 04:15:23 2012 CET by the DBLP Team — Data released under the ODC-BY 1.0 license — See also our legal information page