智云搜索
首页
搜索
文献
期刊
会议
图书
课程
数据分析
学者
主题
机构
期刊
学科
地区
帮助
欢迎您:西北民族大学图书馆
个人账号登录
基本资料
我的订阅
我的收藏
求助记录
退出登录
消息
CPP '25: Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs
CPP '25:第14届ACM Sigplan国际认证计划和证明会议论文集
会议集名称:
CPP: Certified Programs and Proofs(CPP:经认证的计划和证明)
ISBN:
9798400713477
会议时间:
January 20 - 21, 2025
会议地点:
Denver CO USA
出版社:
Association for Computing Machinery
22
总文献数
收藏
导航&检索条件: 整届会议
共计: 22篇
全选
已选
0
篇
导出
以引用结构导出(TXT)
以表格形式导出(Excel)
参考译文
Leakage-Free Probabilistic Jasmin Programs
Leakage-Free Probabilistic Jasmin Programs
会议论文
José Bacelar Almeida[1];Denis Firsov[2];Tiago Oliveira[3];Dominique Unruh[4]
CPP: Certified Programs and Proofs
ISBN: 9798400713477, 2025 年, 卷, 3 - 16 页, DOI: 10.1145/3703595.3705871
CPP:经认证的计划和证明
ISBN: 9798400713477, 2025 年, 卷, 3 - 16 页, DOI: 10.1145/3703595.3705871
机构暂未开通该资源的服务权限,如有疑问请联系图书馆。
文献详情
引用格式导出
发布源
Nominal Matching Logic with Fixpoints
Nominal Matching Logic with Fixpoints
会议论文
Mircea Sebe[1];Maribel Fernández[2];James Cheney[3]
CPP: Certified Programs and Proofs
ISBN: 9798400713477, 2025 年, 卷, 17 - 33 页, DOI: 10.1145/3703595.3705872
CPP:经认证的计划和证明
ISBN: 9798400713477, 2025 年, 卷, 17 - 33 页, DOI: 10.1145/3703595.3705872
机构暂未开通该资源的服务权限,如有疑问请联系图书馆。
文献详情
引用格式导出
发布源
Intrinsically Correct Sorting in Cubical Agda
Intrinsically Correct Sorting in Cubical Agda
会议论文
Cass Alexandru[1];Vikraman Choudhury[2];Jurriaan Rot[3];Niels van der Weide[3]
CPP: Certified Programs and Proofs
ISBN: 9798400713477, 2025 年, 卷, 34 - 49 页, DOI: 10.1145/3703595.3705873
CPP:经认证的计划和证明
ISBN: 9798400713477, 2025 年, 卷, 34 - 49 页, DOI: 10.1145/3703595.3705873
机构暂未开通该资源的服务权限,如有疑问请联系图书馆。
文献详情
引用格式导出
发布源
Certifying Rings of Integers in Number Fields
Certifying Rings of Integers in Number Fields
会议论文
Anne Baanen[1];Alain Chavarri Villarello[2];Sander R. Dahmen[2]
CPP: Certified Programs and Proofs
ISBN: 9798400713477, 2025 年, 卷, 50 - 66 页, DOI: 10.1145/3703595.3705874
CPP:经认证的计划和证明
ISBN: 9798400713477, 2025 年, 卷, 50 - 66 页, DOI: 10.1145/3703595.3705874
机构暂未开通该资源的服务权限,如有疑问请联系图书馆。
文献详情
引用格式导出
发布源
Formalization of Differential Privacy in Isabelle/HOL
Formalization of Differential Privacy in Isabelle/HOL
会议论文
Tetsuya Sato[1];Yasuhiko Minamide[1]
CPP: Certified Programs and Proofs
ISBN: 9798400713477, 2025 年, 卷, 67 - 82 页, DOI: 10.1145/3703595.3705875
CPP:经认证的计划和证明
ISBN: 9798400713477, 2025 年, 卷, 67 - 82 页, DOI: 10.1145/3703595.3705875
机构暂未开通该资源的服务权限,如有疑问请联系图书馆。
文献详情
引用格式导出
发布源
The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic
会议论文
Simon Friis Vindum[1];Aïna Linn Georges[1];Lars Birkedal[1]
CPP: Certified Programs and Proofs
ISBN: 9798400713477, 2025 年, 卷, 83 - 97 页, DOI: 10.1145/3703595.3705876
CPP:经认证的计划和证明
ISBN: 9798400713477, 2025 年, 卷, 83 - 97 页, DOI: 10.1145/3703595.3705876
机构暂未开通该资源的服务权限,如有疑问请联系图书馆。
文献详情
引用格式导出
发布源
Tactic Script Optimisation for Aesop
Tactic Script Optimisation for Aesop
会议论文
Jannis Limperg[1]
CPP: Certified Programs and Proofs
ISBN: 9798400713477, 2025 年, 卷, 98 - 111 页, DOI: 10.1145/3703595.3705877
CPP:经认证的计划和证明
ISBN: 9798400713477, 2025 年, 卷, 98 - 111 页, DOI: 10.1145/3703595.3705877
机构暂未开通该资源的服务权限,如有疑问请联系图书馆。
文献详情
引用格式导出
发布源
A CHERI C Memory Model for Verified Temporal Safety
A CHERI C Memory Model for Verified Temporal Safety
会议论文
Vadim Zaliva[1];Kayvan Memarian[1];Brian Campbell[2];Ricardo Almeida[2];Nathaniel Filardo[1];Ian Stark[2];Peter Sewell[1]
CPP: Certified Programs and Proofs
ISBN: 9798400713477, 2025 年, 卷, 112 - 126 页, DOI: 10.1145/3703595.3705878
CPP:经认证的计划和证明
ISBN: 9798400713477, 2025 年, 卷, 112 - 126 页, DOI: 10.1145/3703595.3705878
机构暂未开通该资源的服务权限,如有疑问请联系图书馆。
文献详情
引用格式导出
发布源
CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq
CertiCoq-Wasm: A Verified WebAssembly Backend for CertiCoq
会议论文
Wolfgang Meier[1];Martin Jensen[1];Jean Pichon-Pharabod[1];Bas Spitters[1]
CPP: Certified Programs and Proofs
ISBN: 9798400713477, 2025 年, 卷, 127 - 139 页, DOI: 10.1145/3703595.3705879
CPP:经认证的计划和证明
ISBN: 9798400713477, 2025 年, 卷, 127 - 139 页, DOI: 10.1145/3703595.3705879
机构暂未开通该资源的服务权限,如有疑问请联系图书馆。
文献详情
引用格式导出
发布源
Formally Verified Hardening of C Programs against Hardware Fault Injection
Formally Verified Hardening of C Programs against Hardware Fault Injection
会议论文
Basile Pesin[1];Sylvain Boulmé[2];David Monniaux[2];Marie-Laure Potet[2]
CPP: Certified Programs and Proofs
ISBN: 9798400713477, 2025 年, 卷, 140 - 155 页, DOI: 10.1145/3703595.3705880
CPP:经认证的计划和证明
ISBN: 9798400713477, 2025 年, 卷, 140 - 155 页, DOI: 10.1145/3703595.3705880
机构暂未开通该资源的服务权限,如有疑问请联系图书馆。
文献详情
引用格式导出
发布源
首页
上一页
1
2
3
下一页
末页