Interactive Theorem Proving - Lecture Notes in Computer Science
Latest Publications

TOTAL DOCUMENTS

35
(FIVE YEARS 0)

H-INDEX

13
(FIVE YEARS 0)

Published By Springer Berlin Heidelberg

9783642140518, 9783642140525
Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

Automated Machine-Checked Hybrid System Safety Proofs

2010 ◽  
pp. 259-274 ◽  
Author(s):  
Herman Geuvers ◽  
Adam Koprowski ◽  
Dan Synek ◽  
Eelis van der Weegen
Keyword(s):  
Hybrid System ◽  
System Safety

A New Foundation for Nominal Isabelle

2010 ◽  
pp. 35-50 ◽  
Author(s):  
Brian Huffman ◽  
Christian Urban

Validating QBF Invalidity in HOL4

2010 ◽  
pp. 466-480 ◽  
Author(s):  
Tjark Weber

Inductive Consequences in the Calculus of Constructions

2010 ◽  
pp. 450-465
Author(s):  
Daria Walukiewicz-Chrząszcz ◽  
Jacek Chrząszcz
Keyword(s):  
Calculus Of Constructions

Equations: A Dependent Pattern-Matching Compiler

2010 ◽  
pp. 419-434 ◽  
Author(s):  
Matthieu Sozeau
Keyword(s):  
Pattern Matching

scholarly journals A Certified Denotational Abstract Interpreter

2010 ◽  
pp. 9-24 ◽  
Author(s):  
David Cachera ◽  
David Pichardie

scholarly journals Formal Proof of a Wave Equation Resolution Scheme: The Method Error

2010 ◽  
pp. 147-162 ◽  
Author(s):  
Sylvie Boldo ◽  
François Clément ◽  
Jean-Christophe Filliâtre ◽  
Micaela Mayero ◽  
Guillaume Melquiond ◽  
...  
Keyword(s):  
Wave Equation ◽  
Formal Proof ◽  
Equation Resolution ◽  
Method Error ◽  
Resolution Scheme

scholarly journals Importing HOL Light into Coq

2010 ◽  
pp. 307-322 ◽  
Author(s):  
Chantal Keller ◽  
Benjamin Werner
Keyword(s):  
Hol Light
Load More ...
Sign in / Sign up

Export Citation Format

Share Document