CPP 2011
28 papers
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- A Proposal for Broad Spectrum Proof Certificates
- Algebra, Logic, Locality, Concurrency
- Automated Certification of Implicit Induction Proofs
- Automatically Verifying Typing Constraints for a Data Processing Language
- Certified Security Proofs of Cryptographic Protocols in the Computational Model: An Application to Intrusion Resilience
- Constructive Formalization of Hybrid Logic with Eventualities
- Coq Mechanization of Featherweight Fortress with Multiple Dispatch and Multiple Inheritance
- Coquet: A Coq Library for Verifying Hardware
- Engineering Theories with Z3
- First Steps towards the Certification of an ARM Simulator Using Compcert
- Formalization of Wu's Simple Method in Coq
- Full Reduction at Full Throttle
- Hardware-Dependent Proofs of Numerical Programs
- Mechanizing the Metatheory of mini-XQuery
- Modular SMT Proofs for Fast Reflexive Checking Inside Coq
- Proof Pearl: The Marriage Theorem
- Proof-Carrying Code in a Session-Typed Process Calculus
- Reasoning about Constants in Nominal Isabelle or How to Formalize the Second Fixed Point Theorem
- Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL
- Simple, Functional, Sound and Complete Parsing for All Context-Free Grammars
- Tactics for Reasoning Modulo AC in Coq
- Teaching Experience: Logic and Formal Methods with Coq
- The Teaching Tool CalcCheck A Proof-Checker for Gries and Schneider's "Logical Approach to Discrete Math"
- Univalent Semantics of Constructive Type Theories
- VeriSmall: Verified Smallfoot Shape Analysis
- Verification of Scalable Synchronous Queue