会员服务
交互 · 设计 · 系统 · 示例 · 设计决策 ·
12 月 23 日
The Design of an Interactive Proof Mode for Dafny
翻译：Dafny交互式证明模式的设计
Ştefan Ciobâcă,K. Rustan M. Leino,Ştefan-Alexandru Mercaş,Roxana-Mihaela Timon
Ştefan Ciobâcă,K. Rustan M. Leino,Ştefan-Alexandru Mercaş,Roxana-Mihaela Timon

We propose to extend the Dafny system with an interactive proof mode. We present a motivating example, how the IPM works, including the main design choices we make, and a prototype implementation.


翻译：本文提出为Dafny系统扩展交互式证明模式。我们通过一个启发性示例，阐述交互式证明模式的工作原理，包括核心设计决策，并展示原型实现方案。
0
下载
关闭预览

相关内容

【NeurIPS2021】用于文本图表示学习的 GNN 嵌套 Transformer 模型：GraphFormers
【NeurIPS2021】用于文本图表示学习的 GNN 嵌套 Transformer 模型：GraphFormers
专知会员服务
46+阅读 · 2021年11月24日
UCM《机器学习导论笔记》，80页pdf CSE176 Introduction to Machine Learning
专知会员服务
31+阅读 · 2021年9月29日
【IJCAI2020】统计相关模型，A Complete Characterization of Projectivity for Statistical Relational Models
【IJCAI2020】统计相关模型，A Complete Characterization of Projectivity for Statistical Relational Models
专知会员服务
20+阅读 · 2020年4月25日
【ICLR 2020】 基于组合的多关系图卷积网络 Composition-Based Multi-Relational Graph Convolutional Networks
【ICLR 2020】 基于组合的多关系图卷积网络 Composition-Based Multi-Relational Graph Convolutional Networks
专知会员服务
108+阅读 · 2020年3月29日
【亚马逊-WWW2020】不解析,生成!用于面向任务的语义分析的序列到序列体系结构，Don't Parse, Generate! A Sequence to Sequence Architecture for Task-Oriented Semantic Parsing
【亚马逊-WWW2020】不解析,生成!用于面向任务的语义分析的序列到序列体系结构，Don't Parse, Generate! A Sequence to Sequence Architecture for Task-Oriented Semantic Parsing
专知会员服务
15+阅读 · 2020年2月1日
图机器学习 2.2-2.4 Properties of Networks, Random Graph
图机器学习 2.2-2.4 Properties of Networks, Random Graph
图与推荐
10+阅读 · 2020年3月28日
【NeurIPS2019】图变换网络：Graph Transformer Network
【NeurIPS2019】图变换网络：Graph Transformer Network
专知
245+阅读 · 2019年11月18日
【AutoML】自动机器学习：最近进展研究综述 AutoML：A survey of State-of-the-art
【AutoML】自动机器学习：最近进展研究综述 AutoML：A survey of State-of-the-art
产业智能官
15+阅读 · 2019年8月13日
Focal Loss for Dense Object Detection
Focal Loss for Dense Object Detection
统计学习与视觉计算组
12+阅读 · 2018年3月15日
Layer Normalization原理及其TensorFlow实现
Layer Normalization原理及其TensorFlow实现
深度学习每日摘要
32+阅读 · 2017年6月17日
Musielak-Orlicz-Sobolev 空间中的迹嵌入及其应用
国家自然科学基金
2+阅读 · 2015年12月31日
Schr？dinger-Poisson方程守恒DDG方法研究
国家自然科学基金
2+阅读 · 2015年12月31日
动态Gr？bner 基与GVW算法
国家自然科学基金
0+阅读 · 2014年12月31日
Biot模型基于有限元离散的多重网格算法研究
国家自然科学基金
1+阅读 · 2014年12月31日
Poisson流形上的修正Hamilton方法
国家自然科学基金
0+阅读 · 2014年12月31日
Note on a Translation from First-Order Logic into the Calculus of Relations Preserving Validity and Finite Validity
Arxiv
0+阅读 · 12月24日
Multi-LLM Thematic Analysis with Dual Reliability Metrics: Combining Cohen's Kappa and Semantic Similarity for Qualitative Research Validation
Arxiv
0+阅读 · 12月23日
CBA: Communication-Bound-Aware Cross-Domain Resource Assignment for Pipeline-Parallel Distributed LLM Training in Dynamic Multi-DC Optical Networks
Arxiv
0+阅读 · 12月23日
MDToC: Metacognitive Dynamic Tree of Concepts for Boosting Mathematical Problem-Solving of Large Language Models
Arxiv
0+阅读 · 12月21日
New Hybrid Heuristics for Pseudo-Boolean Propagation
Arxiv
0+阅读 · 12月19日
VIP会员
文章信息
前往arXiv
下载PDF
相关主题
交互
设计
系统
示例
设计决策
相关VIP内容
【NeurIPS2021】用于文本图表示学习的 GNN 嵌套 Transformer 模型：GraphFormers
【NeurIPS2021】用于文本图表示学习的 GNN 嵌套 Transformer 模型：GraphFormers
专知会员服务
46+阅读 · 2021年11月24日
UCM《机器学习导论笔记》，80页pdf CSE176 Introduction to Machine Learning
专知会员服务
31+阅读 · 2021年9月29日
【IJCAI2020】统计相关模型，A Complete Characterization of Projectivity for Statistical Relational Models
【IJCAI2020】统计相关模型，A Complete Characterization of Projectivity for Statistical Relational Models
专知会员服务
20+阅读 · 2020年4月25日
【ICLR 2020】 基于组合的多关系图卷积网络 Composition-Based Multi-Relational Graph Convolutional Networks
【ICLR 2020】 基于组合的多关系图卷积网络 Composition-Based Multi-Relational Graph Convolutional Networks
专知会员服务
108+阅读 · 2020年3月29日
【亚马逊-WWW2020】不解析,生成!用于面向任务的语义分析的序列到序列体系结构，Don't Parse, Generate! A Sequence to Sequence Architecture for Task-Oriented Semantic Parsing
【亚马逊-WWW2020】不解析,生成!用于面向任务的语义分析的序列到序列体系结构，Don't Parse, Generate! A Sequence to Sequence Architecture for Task-Oriented Semantic Parsing
专知会员服务
15+阅读 · 2020年2月1日
热门VIP内容
相关资讯
图机器学习 2.2-2.4 Properties of Networks, Random Graph
图机器学习 2.2-2.4 Properties of Networks, Random Graph
图与推荐
10+阅读 · 2020年3月28日
【NeurIPS2019】图变换网络：Graph Transformer Network
【NeurIPS2019】图变换网络：Graph Transformer Network
专知
245+阅读 · 2019年11月18日
【AutoML】自动机器学习：最近进展研究综述 AutoML：A survey of State-of-the-art
【AutoML】自动机器学习：最近进展研究综述 AutoML：A survey of State-of-the-art
产业智能官
15+阅读 · 2019年8月13日
Focal Loss for Dense Object Detection
Focal Loss for Dense Object Detection
统计学习与视觉计算组
12+阅读 · 2018年3月15日
Layer Normalization原理及其TensorFlow实现
Layer Normalization原理及其TensorFlow实现
深度学习每日摘要
32+阅读 · 2017年6月17日
相关论文
Note on a Translation from First-Order Logic into the Calculus of Relations Preserving Validity and Finite Validity
Arxiv
0+阅读 · 12月24日
Multi-LLM Thematic Analysis with Dual Reliability Metrics: Combining Cohen's Kappa and Semantic Similarity for Qualitative Research Validation
Arxiv
0+阅读 · 12月23日
CBA: Communication-Bound-Aware Cross-Domain Resource Assignment for Pipeline-Parallel Distributed LLM Training in Dynamic Multi-DC Optical Networks
Arxiv
0+阅读 · 12月23日
MDToC: Metacognitive Dynamic Tree of Concepts for Boosting Mathematical Problem-Solving of Large Language Models
Arxiv
0+阅读 · 12月21日
New Hybrid Heuristics for Pseudo-Boolean Propagation
Arxiv
0+阅读 · 12月19日
相关基金
Musielak-Orlicz-Sobolev 空间中的迹嵌入及其应用
国家自然科学基金
2+阅读 · 2015年12月31日
Schr？dinger-Poisson方程守恒DDG方法研究
国家自然科学基金
2+阅读 · 2015年12月31日
动态Gr？bner 基与GVW算法
国家自然科学基金
0+阅读 · 2014年12月31日
Biot模型基于有限元离散的多重网格算法研究
国家自然科学基金
1+阅读 · 2014年12月31日
Poisson流形上的修正Hamilton方法
国家自然科学基金
0+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员
Top