default search action

combined dblp search
author search
venue search
publication search

ask others

CPP 2013: Melbourne, Victoria, Australia

> 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/2013
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/2013
Georges Gonthier, Michael Norrish:
Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings. Lecture Notes in Computer Science 8307, Springer 2013, ISBN 978-3-319-03544-4

Invited Lectures

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/LicataB13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/LicataB13
Daniel R. Licata, Guillaume Brunerie:
π n (S n ) in Homotopy Type Theory. 1-16

Session 1: Code Verification

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/DoddsA13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/DoddsA13
Josiah Dodds, Andrew W. Appel:
Mostly Sound Type System Improves a Foundational Program Verifier. 17-32
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Stewart13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Stewart13
Gordon Stewart:
Computational Verification of Network Programs in Coq. 33-49
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Krebbers13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Krebbers13
Robbert Krebbers:
Aliasing Restrictions of C11 Formalized in Coq. 50-65

Session 2: Elegant Proofs

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/MyreenC13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/MyreenC13
Magnus O. Myreen, Gregorio Curello:
Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code. 66-81
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/DoczkalKS13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/DoczkalKS13
Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka:
A Constructive Theory of Regular Languages in Coq. 82-97
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/FirsovU13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/FirsovU13
Denis Firsov, Tarmo Uustalu:
Certified Parsing of Regular Languages. 98-113

Session 3: Proof Libraries

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/SchroppP13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/SchroppP13
Andreas Schropp, Andrei Popescu:
Nonfree Datatypes in Isabelle/HOL - Animating a Many-Sorted Metatheory. 114-130
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/HuffmanK13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/HuffmanK13
Brian Huffman, Ondrej Kuncar:
Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. 131-146
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/CohenDM13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/CohenDM13
Cyril Cohen, Maxime Dénès, Anders Mörtberg:
Refinements for Free! 147-162

Session 4: Mathematics

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Asperti13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Asperti13
Andrea Asperti:
A Formal Proof of Borodin-Trakhtenbrot's Gap Theorem. 163-177
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Sternagel13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Sternagel13
Christian Sternagel:
Certified Kruskal's Tree Theorem. 178-193
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/MillerT13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/MillerT13
Dale Miller, Alwen Tiu:
Extracting Proofs from Tabled Proof Search. 194-210

Session 5: Certified Transformations

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/HuangM13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/HuangM13
Daniel Huang, Greg Morrisett:
Formalizing the SAFECode Type System. 211-226
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/Bell13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/Bell13
Christian J. Bell:
Certifiably Sound Parallelizing Transformations. 227-242
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/BelangerMP13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/BelangerMP13
Olivier Savary Bélanger, Stefan Monnier, Brigitte Pientka:
Programming Type-Safe Transformations Using Higher-Order Abstract Syntax. 243-258

Session 6: Security

- view
  authority control:
- export record
  dblp key:
  - conf/cpp/0001HN13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/0001HN13
Andrei Popescu, Johannes Hölzl, Tobias Nipkow:
Formalizing Probabilistic Noninterference. 259-275
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/KhakpourSD13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/KhakpourSD13
Narges Khakpour, Oliver Schwarz, Mads Dam:
Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties. 276-291
- view
  authority control:
- export record
  dblp key:
  - conf/cpp/WuZU13
- ask others
- share record
  persistent URL:
  - https://dblp.org/rec/conf/cpp/WuZU13
Chunhan Wu, Xingyuan Zhang, Christian Urban:
A Formal Model and Correctness Proof for an Access Control Policy Framework. 292-307

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.