Interactive Theorem Proving - Lecture Notes in Computer Science
Latest Publications

TOTAL DOCUMENTS

(FIVE YEARS 0)

H-INDEX

(FIVE YEARS 0)

Published By Springer International Publishing

9783319431437, 9783319431444

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

Proof Pearl: Bounding Least Common Multiples with Triangles

Interactive Theorem Proving - Lecture Notes in Computer Science ◽

10.1007/978-3-319-43144-4_9 ◽

2016 ◽

pp. 140-150

Author(s):

Hing-Lun Chan ◽

Michael Norrish

Download Full-text

CoqPIE: An IDE Aimed at Improving Proof Development Productivity

Interactive Theorem Proving - Lecture Notes in Computer Science ◽

10.1007/978-3-319-43144-4_32 ◽

2016 ◽

pp. 491-499 ◽

Cited By ~ 3

Author(s):

Kenneth Roe ◽

Scott Smith

Download Full-text

Equational Reasoning with Applicative Functors

Interactive Theorem Proving - Lecture Notes in Computer Science ◽

10.1007/978-3-319-43144-4_16 ◽

2016 ◽

pp. 252-273 ◽

Cited By ~ 3

Author(s):

Andreas Lochbihler ◽

Joshua Schneider

Keyword(s):

Equational Reasoning

Download Full-text

Cardinalities of Finite Relations in Coq

Interactive Theorem Proving - Lecture Notes in Computer Science ◽

10.1007/978-3-319-43144-4_29 ◽

2016 ◽

pp. 466-474 ◽

Cited By ~ 4

Author(s):

Paul Brunet ◽

Damien Pous ◽

Insa Stucke

Download Full-text

An Isabelle/HOL Formalisation of Green’s Theorem

Interactive Theorem Proving - Lecture Notes in Computer Science ◽

10.1007/978-3-319-43144-4_1 ◽

2016 ◽

pp. 3-19 ◽

Cited By ~ 1

Author(s):

Mohammad Abdulaziz ◽

Lawrence C. Paulson

Keyword(s):

Green's Theorem ◽

Green’S Theorem

Download Full-text

POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)

Interactive Theorem Proving - Lecture Notes in Computer Science ◽

10.1007/978-3-319-43144-4_5 ◽

2016 ◽

pp. 69-86 ◽

Cited By ~ 3

Author(s):

Fahad Ausaf ◽

Roy Dyckhoff ◽

Christian Urban

Keyword(s):

Regular Expressions ◽

Derivatives Of

Download Full-text

Infeasible Paths Elimination by Symbolic Execution Techniques

Interactive Theorem Proving - Lecture Notes in Computer Science ◽

10.1007/978-3-319-43144-4_3 ◽

2016 ◽

pp. 36-51 ◽

Cited By ~ 2

Author(s):

Romain Aissat ◽

Frédéric Voisin ◽

Burkhart Wolff

Keyword(s):

Symbolic Execution

Download Full-text

What’s in a Theorem Name?

Interactive Theorem Proving - Lecture Notes in Computer Science ◽

10.1007/978-3-319-43144-4_28 ◽

2016 ◽

pp. 459-465 ◽

Cited By ~ 3

Author(s):

David Aspinall ◽

Cezary Kaliszyk

Download Full-text

AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic

Interactive Theorem Proving - Lecture Notes in Computer Science ◽

10.1007/978-3-319-43144-4_27 ◽

2016 ◽

pp. 441-456 ◽

Cited By ~ 3

Author(s):

Bohua Zhan

Keyword(s):

Higher Order ◽

Order Logic ◽

Higher Order Logic

Download Full-text

Formalizing the Edmonds-Karp Algorithm

Interactive Theorem Proving - Lecture Notes in Computer Science ◽

10.1007/978-3-319-43144-4_14 ◽

2016 ◽

pp. 219-234 ◽

Cited By ~ 7

Author(s):

Peter Lammich ◽

S. Reza Sefidgar

Download Full-text

Interactive Theorem Proving - Lecture Notes in Computer ScienceLatest Publications

TOTAL DOCUMENTS

H-INDEX

Published By Springer International Publishing

Proof Pearl: Bounding Least Common Multiples with Triangles

CoqPIE: An IDE Aimed at Improving Proof Development Productivity

Equational Reasoning with Applicative Functors

Cardinalities of Finite Relations in Coq

An Isabelle/HOL Formalisation of Green’s Theorem

POSIX Lexing with Derivatives of Regular Expressions (Proof Pearl)

Infeasible Paths Elimination by Symbolic Execution Techniques

What’s in a Theorem Name?

AUTO2, A Saturation-Based Heuristic Prover for Higher-Order Logic

Formalizing the Edmonds-Karp Algorithm

Interactive Theorem Proving - Lecture Notes in Computer Science
Latest Publications