首页>外文会议>International conference on certified programs and proofs

International conference on certified programs and proofs

召开年：2013
召开地：Melbourne(AU)
出版时间：-

会议文集：-

会议论文

热门论文

全部论文

全选（0）

1.π_n(S~n) in Homotopy Type Theory

机译：同伦型理论中的π_n（S〜n）
- 作者：Daniel R. Licata;Guillaume Brunerie
- 会议名称：《》 | 2013年
2.Mostly Sound Type System Improves a Foundational Program Verifier

机译：大多数声音类型系统改进了基础程序验证程序
- 作者：Josiah Dodds;Andrew W. Appel
- 会议名称：《International conference on certified programs and proofs》 | 2013年
3.Computational Verification of Network Programs in Coq

机译：Coq中网络程序的计算验证
- 作者：Gordon Stewart
- 会议名称：《International conference on certified programs and proofs》 | 2013年
4.Aliasing Restrictions of C11 Formalized in Coq

机译：Coq中正式化的C11的别名限制
- 作者：Robbert Krebbers
- 会议名称：《International conference on certified programs and proofs》 | 2013年
5.Proof Pearl: A Verified Bignum Implementation in x86-64 Machine Code

机译：Proof Pearl：x86-64机器代码中经过验证的Bignum实现
- 作者：Magnus O. Myreen;Gregorio Curello
- 会议名称：《International conference on certified programs and proofs》 | 2013年
6.A Constructive Theory of Regular Languages in Coq

机译：Coq中常规语言的建构理论
- 作者：Christian Doczkal;Jan-Oliver Kaiser;Gert Smolka
- 会议名称：《International conference on certified programs and proofs》 | 2013年
- regular languages;
- regular expressions;
- finite automata;
- Myhill-Nerode;
- Coq;
- Ssreflect;
7.Certified Parsing of Regular Languages

机译：认证的常规语言解析
- 作者：Denis Firsov;Tarmo Uustalu
- 会议名称：《International conference on certified programs and proofs》 | 2013年
8.Nonfree Datatypes in Isabelle/HOL Animating a Many-Sorted Metatheory

机译：Isabelle / HOL中的非自由数据类型对多分类元理论进行了动画处理
- 作者：Andreas Schropp;Andrei Popescu
- 会议名称：《International conference on certified programs and proofs》 | 2013年
9.Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL

机译：提升和转移：Isabelle / HOL中商数的模块化设计
- 作者：Brian Huffman;Ondrej Kuncar
- 会议名称：《International conference on certified programs and proofs》 | 2013年
10.Refinements for Free!

机译：免费优化！
- 作者：Cyril Cohen;Maxime Denes;Anders Moertberg
- 会议名称：《International conference on certified programs and proofs》 | 2013年
- Coq;
- Data refinements;
- Formal proofs;
- Efficient algorithms and data structures;
- Parametricity;
11.A Formal Proof of Borodin-Trakhtenbrot's Gap Theorem

机译：Borodin-Trakhtenbrot间隙定理的形式证明
- 作者：Andrea Asperti
- 会议名称：《International conference on certified programs and proofs》 | 2013年
12.Certified Kruskal's Tree Theorem

机译：认证的Kruskal树定理
- 作者：Christian Sternagel
- 会议名称：《International conference on certified programs and proofs》 | 2013年
- Well-Quasi-Orders;
- Dickson's Lemma;
- Minimal Bad Sequences;
- Higman's Lemma;
- Kruskal's Tree Theorem;
13.Extracting Proofs from Tabled Proof Search

机译：从表式证明搜索中提取证明
- 作者：Dale Miller;Alwen Tiu
- 会议名称：《International conference on certified programs and proofs》 | 2013年
14.Formalizing the SAFECode Type System

机译：正式制定SAFECode类型系统
- 作者：Daniel Huang;Greg Morrisett
- 会议名称：《International conference on certified programs and proofs》 | 2013年
- verification;
- SAFECode;
- LLVM;
- memory safety;
15.Certifiably Sound Parallelizing Transformations

机译：可验证的声音并行转换
- 作者：Christian J. Bell
- 会议名称：《International conference on certified programs and proofs》 | 2013年
16.Programming Type-Safe Transformations Using Higher-Order Syntax

机译：使用高阶语法对类型安全的转换进行编程
- 作者：Olivier Savary-Belanger;Stefan Monnier;Brigitte Pientka
- 会议名称：《International conference on certified programs and proofs》 | 2013年
17.Formalizing Probabilistic Noninterference

机译：形式化概率非干扰
- 作者：Andrei Popescu;Johannes Hoelzl;Tobias Nipkow
- 会议名称：《》 | 2013年
18.Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties

机译：机器辅助的ARMv7指令级别隔离属性证明
- 作者：Narges Khakpour;Oliver Schwarz;Mads Dam
- 会议名称：《International conference on certified programs and proofs》 | 2013年
- ARM instruction set;
- noninterference;
- user mode execution;
- kernel security;
- theorem proving;
19.A Formal Model and Correctness Proof for an Access Control Policy Framework

机译：访问控制策略框架的正式模型和正确性证明
- 作者：Chunhan Wu;Xingyuan Zhang;Christian Urban
- 会议名称：《International conference on certified programs and proofs》 | 2013年
20.Preface

机译：前言
- 作者：Georges Gonthier;Michael Norrish
- 会议名称：《International conference on certified programs and proofs》 | 2013年
21.The 'Probabilistic Information-Order for Noninterference' Competition: Do we have a winner?

机译：“无干扰的概率信息顺序”竞赛：我们有赢家吗？
- 作者：Carroll Morgan
- 会议名称：《International conference on certified programs and proofs》 | 2013年