首页>外文会议>其他>Interactive theorem proving

Interactive theorem proving

召开年：
召开地：
出版时间：-

会议文集：-

会议论文

热门论文

全部论文

全选（0）

1.Deductive Program Verification

机译：演绎程序验证
- 作者：Jean-Christophe Filliatre
- 会议名称：《Interactive theorem proving》 | 2018年
- Deductive verification;
- Theorem proving;
2.Mike Gordon: Tribute to a Pioneer in Theorem Proving and Formal Verification

机译：Mike Gordon：向定理证明和形式验证的先驱致敬
- 作者：John Harrison
- 会议名称：《Interactive theorem proving》 | 2018年
3.Towards Certified Meta-Programming with Typed Template-Coq

机译：使用类型化的模板-Coq实现认证的元编程
- 作者：Abhishek Anand;Simon Boulier;Cyril Cohen;Matthieu Sozeau;Nicolas Tabareau
- 会议名称：《Interactive theorem proving》 | 2018年
4.Software Tool Support for Modular Reasoning in Modal Logics of Actions

机译：动作模态逻辑中模块化推理的软件工具支持
- 作者：Samuel Balco;Sabine Frittella;Giuseppe Greco;Alexander Kurz;Alessandra Palmigiano
- 会议名称：《Interactive theorem proving》 | 2018年
5.A Coq Tactic for Equality Learning in Linear Arithmetic

机译：线性算法中平等学习的Coq策略
- 作者：Sylvain Boulme;Alexandre Marechal
- 会议名称：《Interactive theorem proving》 | 2018年
6.Tactics and Certificates in Meta Dedukti

机译：Meta Dedukti中的策略和证书
- 作者：Raphaeel Cauderlier
- 会议名称：《Interactive theorem proving》 | 2018年
7.A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs

机译：树宽两个图的次要排除属性的形式证明
- 作者：Christian Doczkal;Guillaume Combette;Damien Pous
- 会议名称：《Interactive theorem proving》 | 2018年
- Graph theory;
- Graph minor theorem;
- Coq;
- Ssreflect;
8.HOL Light QE

机译：HOL Light QE
- 作者：Jacques Carette;William M. Farmer;Patrick Laskowski
- 会议名称：《Interactive theorem proving》 | 2018年
9.Verification of PCP-Related Computational Reductions in Coq

机译：验证Coq中与PCP相关的计算减少
- 作者：Yannick Forster;Edith Heiter;Gert Smolka
- 会议名称：《Interactive theorem proving》 | 2018年
10.ProofWatch: Watchlist Guidance for Large Theories in E

机译：ProofWatch：E中大型理论的监视列表指南
- 作者：Zarathustra Goertzel;Jan Jakubuv;Stephan Schulz;Josef Urban
- 会议名称：《Interactive theorem proving》 | 2018年
11.Verifying the LTL to Biichi Automata Translation via Very Weak Alternating Automata

机译：通过非常弱的交替自动机验证LTL到Biichi自动机翻译
- 作者：Simon Jantsch;Michael Norrish
- 会议名称：《Interactive theorem proving》 | 2018年
12.Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY

机译：了解演绎验证的参数：KeY的经验研究
- 作者：Alexander Knueppel;Thomas Thuem;Carsten Immanuel Pardylla;Ina Schaefer
- 会议名称：《Interactive theorem proving》 | 2018年
- Deductive verification;
- Design by contract Formal methods;
- Theorem proving;
- KeY;
- Control parameters Automated reasoning;
13.Proof Pearl: Constructive Extraction of Cycle Finding Algorithms

机译：Proof Pearl：周期发现算法的构造性提取
- 作者：Dominique Larchey-Wendling
- 会议名称：《Interactive theorem proving》 | 2018年
- Cycle finding;
- Bar inductive predicates Partial algorithms in Coq;
- Correctness by extraction;
14.Relational Parametricity and Quotient Preservation for Modular (Co)datatypes

机译：模块化（Co）数据类型的关系参数和商数保留
- 作者：Andreas Lochbihler;Joshua Schneider
- 会议名称：《Interactive theorem proving》 | 2018年
15.Formalizing Implicative Algebras in Coq

机译：形式化Coq中的隐含代数
- 作者：Etienne Miquey
- 会议名称：《Interactive theorem proving》 | 2018年
16.Towards Formal Foundations for Game Theory

机译：建立博弈论的正式基础
- 作者：Julian Parsert;Cezary Kaliszyk
- 会议名称：《Interactive theorem proving》 | 2018年
17.A Formal Equational Theory for Call-By-Push-Value

机译：呼叫按值的形式方程理论
- 作者：Christine Rizkallah;Dmitri Garbuzov;Steve Zdancewic
- 会议名称：《Interactive theorem proving》 | 2018年
18.Verified Tail Bounds for Randomized Programs

机译：已验证的随机程序的尾巴界限
- 作者：Joseph Tassarotti;Robert Harper
- 会议名称：《Interactive theorem proving》 | 2018年
19.MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)

机译：MDP + TA = PTA：概率定时自动机，形式化（简短论文）
- 作者：Simon Wimmer;Johannes Hoelzl
- 会议名称：《Interactive theorem proving》 | 2018年
20.Formalization of a Polymorphic Subtyping Algorithm

机译：多态子类型化算法的形式化
- 作者：Jinxu Zhao;Bruno C. d. S. Oliveira;Tom Schrijvers
- 会议名称：《Interactive theorem proving》 | 2018年
21.Preface

机译：前言
- 作者：Jeremy Avigad;Assia Mahboubi
- 会议名称：《Interactive theorem proving》 | 2018年
22.Voevodsky's Work on Formalization of Proofs and the Foundations of Mathematics

机译：Voevodsky的证明形式化工作和数学基础
- 作者：Daniel R. Grayson
- 会议名称：《Interactive theorem proving》 | 2018年
23.Physical Addressing on Real Hardware in Isabelle/HOL

机译：Isabelle / HOL中实际硬件上的物理寻址
- 作者：Reto Achermann;Lukas Humbel;David Cock;Timothy Roscoe
- 会议名称：《Interactive theorem proving》 | 2018年
24.Formalizing Ring Theory in PVS

机译：PVS中的形式化环理论
- 作者：Andreia B. Avelar da Silva;Thaynara Arielly de Lima;Andre Luiz Galdino
- 会议名称：《Interactive theorem proving》 | 2018年
25.Backwards and Forwards with Separation Logic

机译：分离逻辑的前进和后退
- 作者：Callum Bannister;Peter Hoefner;Gerwin Klein
- 会议名称：《Interactive theorem proving》 | 2018年
26.A Coq Formalisation of SQL's Execution Engines

机译：SQL执行引擎的Coq形式化
- 作者：V. Benzaken;E. Contejean;Ch. Keller;E. Martins
- 会议名称：《Interactive theorem proving》 | 2018年
27.The Coinductive Formulation of Common Knowledge

机译：共同知识的归纳表述
- 作者：Colm Baston;Venanzio Capretta
- 会议名称：《Interactive theorem proving》 | 2018年
28.A Formalization of the LLL Basis Reduction Algorithm

机译：LLL基减少算法的形式化
- 作者：Jose Divason;Sebastiaan Joosten;Rene Thiemann;Akihisa Yamada
- 会议名称：《Interactive theorem proving》 | 2018年
29.Verified Analysis of Random Binary Tree Structures

机译：随机二叉树结构的验证分析
- 作者：Manuel Eberl;Max W. Haslbeck;Tobias Nipkow
- 会议名称：《Interactive theorem proving》 | 2018年
30.Efficient Mendler-Style Lambda-Encodings in Cedille

机译：Cedille中的高效Mendler样式Lambda编码
- 作者：Denis Firsov;Richard Blair;Aaron Stump
- 会议名称：《Interactive theorem proving》 | 2018年
- Type theory;
- Lambda-encodings;
- Cedille Induction principle;
- Predecessor function;
- Inductive datatypes;
31.Reification by Parametricity Fast Setup for Proof by Reflection, in Two Lines of Ltac

机译：在两行Ltac中通过参数化进行快速验证以进行反射验证
- 作者：Jason Gross;Andres Erbsen;Adam Chlipala
- 会议名称：《Interactive theorem proving》 | 2018年
32.C_(ALC)C_（HECK）: A Proof Checker for Teaching the 'Logical Approach to Discrete Math'

机译：C_（ALC）C_（HECK）：用于证明“离散数学的逻辑方法”的证明检查器
- 作者：Wolfram Kahl
- 会议名称：《Interactive theorem proving》 | 2018年
33.Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB (Short Paper)

机译：使用ITP进行软件验证应使用二进制代码提取来减少TCB（简短论文）
- 作者：Ramana Kumar;Eric Mullen;Zachary Tatlock;Magnus O. Myreen
- 会议名称：《Interactive theorem proving》 | 2018年
34.Fast Machine Words in Isabelle/HOL

机译：Isabelle / HOL中的快速机器词
- 作者：Andreas Lochbihler
- 会议名称：《Interactive theorem proving》 | 2018年
35.Towards Verified Handwritten Calculational Proofs (Short Paper)

机译：迈向经过验证的手写计算证明（简短论文）
- 作者：Alexandra Mendes;Joao F. Ferreira
- 会议名称：《Interactive theorem proving》 | 2018年
- Handwritten mathematics;
- Interactive theorem proving Mathematical proof;
- Calculational method;
- Handwriting;
36.A Formally Verified Solver for Homogeneous Linear Diophantine Equations

机译：齐次线性丢番图方程的形式验证公式
- 作者：Florian Messner;Julian Parsert;Jonas Schoepf;Christian Sternagel
- 会议名称：《Interactive theorem proving》 | 2018年
37.Boosting the Reuse of Formal Specifications

机译：促进形式规范的重用
- 作者：Mariano M. Moscato;Carlos G. Lopez Pombo;Cesar A. Munoz;Marco A. Feliu
- 会议名称：《Interactive theorem proving》 | 2018年
38.Verified Timing Transformations in Synchronous Circuits with λπ -Ware

机译：带有λπ-Ware的同步电路中经过验证的时序变换
- 作者：Joao Paulo Pizani Flor;Wouter Swierstra
- 会议名称：《Interactive theorem proving》 | 2018年
39.Program Verification in the Presence of Cached Address Translation

机译：存在缓存地址转换的程序验证
- 作者：Hira Taqdees Syeda;Gerwin Klein
- 会议名称：《Interactive theorem proving》 | 2018年
40.Verified Memorization and Dynamic Programming

机译：经过验证的记忆和动态编程
- 作者：Simon Wimmer;Shuwei Hu;Tobias Nipkow
- 会议名称：《Interactive theorem proving》 | 2018年
41.An Agda Formalization of UEresin and Dubois' Asynchronous Fixed-Point Theory

机译：UEresin和Dubois的异步定点理论的Agda形式化
- 作者：Ran Zmigrod;Matthew L. Daggitt;Timothy G. Griffin
- 会议名称：《Interactive theorem proving》 | 2018年