Certified Programs and Proofs - Lecture Notes in Computer Science
Latest Publications

TOTAL DOCUMENTS

19

(FIVE YEARS 0)

H-INDEX

7

(FIVE YEARS 0)

Published By Springer International Publishing

9783319035444, 9783319035451

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

Certifiably Sound Parallelizing Transformations

Certified Programs and Proofs - Lecture Notes in Computer Science ◽

10.1007/978-3-319-03545-1_15 ◽

2013 ◽

pp. 227-242

Author(s):

Christian J. Bell

Download Full-text

Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL

Certified Programs and Proofs - Lecture Notes in Computer Science ◽

10.1007/978-3-319-03545-1_9 ◽

2013 ◽

pp. 131-146 ◽

Author(s):

Brian Huffman ◽

Ondřej Kunčar

Keyword(s):

Download Full-text

A Formal Model and Correctness Proof for an Access Control Policy Framework

Certified Programs and Proofs - Lecture Notes in Computer Science ◽

10.1007/978-3-319-03545-1_19 ◽

2013 ◽

pp. 292-307

Author(s):

Chunhan Wu ◽

Xingyuan Zhang ◽

Christian Urban

Keyword(s):

Access Control ◽

Formal Model ◽

Control Policy ◽

Policy Framework ◽

Access Control Policy ◽

Correctness Proof

Download Full-text

π n (S n ) in Homotopy Type Theory

Certified Programs and Proofs - Lecture Notes in Computer Science ◽

10.1007/978-3-319-03545-1_1 ◽

2013 ◽

pp. 1-16 ◽

Author(s):

Daniel R. Licata ◽

Guillaume Brunerie

Keyword(s):

Homotopy Type ◽

Type Theory ◽

Homotopy Type Theory

Download Full-text

Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties

Certified Programs and Proofs - Lecture Notes in Computer Science ◽

10.1007/978-3-319-03545-1_18 ◽

2013 ◽

pp. 276-291 ◽

Author(s):

Narges Khakpour ◽

Oliver Schwarz ◽

Mads Dam

Download Full-text

Mostly Sound Type System Improves a Foundational Program Verifier

Certified Programs and Proofs - Lecture Notes in Computer Science ◽

10.1007/978-3-319-03545-1_2 ◽

2013 ◽

pp. 17-32 ◽

Author(s):

Josiah Dodds ◽

Andrew W. Appel

Keyword(s):

Download Full-text

Refinements for Free!

Certified Programs and Proofs - Lecture Notes in Computer Science ◽

10.1007/978-3-319-03545-1_10 ◽

2013 ◽

pp. 147-162 ◽

Author(s):

Cyril Cohen ◽

Maxime Dénès ◽

Anders Mörtberg

Download Full-text

Programming Type-Safe Transformations Using Higher-Order Abstract Syntax

Certified Programs and Proofs - Lecture Notes in Computer Science ◽

10.1007/978-3-319-03545-1_16 ◽

2013 ◽

pp. 243-258 ◽

Author(s):

Olivier Savary-Belanger ◽

Stefan Monnier ◽

Brigitte Pientka

Keyword(s):

Higher Order ◽

Abstract Syntax

Download Full-text

Nonfree Datatypes in Isabelle/HOL

Certified Programs and Proofs - Lecture Notes in Computer Science ◽

10.1007/978-3-319-03545-1_8 ◽

2013 ◽

pp. 114-130 ◽

Author(s):

Andreas Schropp ◽

Andrei Popescu

Download Full-text

Formalizing Probabilistic Noninterference

Certified Programs and Proofs - Lecture Notes in Computer Science ◽

10.1007/978-3-319-03545-1_17 ◽

2013 ◽

pp. 259-275 ◽

Author(s):

Andrei Popescu ◽

Johannes Hölzl ◽

Tobias Nipkow

Download Full-text