×

zbMATH — the first resource for mathematics

Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings. (English) Zbl 1195.68009
Lecture Notes in Computer Science 6172. Berlin: Springer (ISBN 978-3-642-14051-8/pbk). xi, 495 p. (2010).

Show indexed articles as search result.

The articles of this volume will be reviewed individually.
Indexed articles:
Cachera, David; Pichardie, David, A certified denotational abstract interpreter, 9-24 [Zbl 1291.68331]
Cowles, John; Gamboa, Ruben, Using a first order logic to verify that some set of reals has no Lesbegue measure, 25-34 [Zbl 1291.68335]
Huffman, Brian; Urban, Christian, A new foundation for Nominal Isabelle, 35-50 [Zbl 1291.68350]
Kumar, Ramana; Norrish, Michael, (Nominal) unification by recursive descent with triangular substitutions, 51-66 [Zbl 1291.68356]
Verbeek, Freek; Schmaltz, Julien, A formal proof of a necessary and sufficient condition for deadlock-free adaptive networks, 67-82 [Zbl 1291.68373]
Armand, Michaël; Grégoire, Benjamin; Spiwack, Arnaud; Théry, Laurent, Extending Coq with imperative features and its application to SAT verification, 83-98 [Zbl 1291.68318]
Autexier, Serge; Dietrich, Dominik, A tactic language for declarative proofs, 99-114 [Zbl 1291.68320]
Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago, Programming language techniques for cryptographic proofs, 115-130 [Zbl 1291.68323]
Blanchette, Jasmin Christian; Nipkow, Tobias, Nitpick: a counterexample generator for higher-order logic based on a relational model finder, 131-146 [Zbl 1291.68326]
Boldo, Sylvie; Clément, François; Filliâtre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre, Formal proof of a wave equation resolution scheme: the method error, 147-162 [Zbl 1291.68329]
Braibant, Thomas; Pous, Damien, An efficient Coq tactic for deciding Kleene algebras, 163-178 [Zbl 1291.68330]
Böhme, Sascha; Weber, Tjark, Fast LCF-style proof reconstruction for Z3, 179-194 [Zbl 1291.68328]
Charguéraud, Arthur, The optimal fixed point combinator, 195-210 [Zbl 1291.68332]
Dufourd, Jean-François; Bertot, Yves, Formal study of plane Delaunay triangulation, 211-226 [Zbl 1291.68337]
Felty, Amy; Pientka, Brigitte, Reasoning with higher-order abstract syntax and contexts: a comparison, 227-242 [Zbl 1291.68340]
Fox, Anthony; Myreen, Magnus O., A trustworthy monadic formalization of the ARMv7 instruction set architecture, 243-258 [Zbl 1291.68341]
Geuvers, Herman; Koprowski, Adam; Synek, Dan; van der Weegen, Eelis, Automated machine-checked hybrid system safety proofs, 259-274 [Zbl 1291.68343]
Hendrix, Joe; Kapur, Deepak; Meseguer, José, Coverset induction with partiality and subsorts: a powerlist case study, 275-290 [Zbl 1291.68346]
Johansson, Moa; Dixon, Lucas; Bundy, Alan, Case-analysis for rippling and inductive proof, 291-306 [Zbl 1291.68352]
Keller, Chantal; Werner, Benjamin, Importing HOL Light into Coq, 307-322 [Zbl 1291.68353]
Krauss, Alexander; Schropp, Andreas, A mechanized translation from higher-order logic to set theory, 323-338 [Zbl 1291.68355]
Lammich, Peter; Lochbihler, Andreas, The Isabelle collections framework, 339-354 [Zbl 1291.68357]
Manolios, Panagiotis; Vroon, Daron, Interactive termination proofs using termination cores, 355-370 [Zbl 1291.68359]
Mansky, William; Gunter, Elsa, A framework for formal verification of compiler optimizations, 371-386 [Zbl 1291.68360]
Mhamdi, Tarek; Hasan, Osman; Tahar, Sofiène, On the formalization of the Lebesgue integration theory in HOL, 387-402 [Zbl 1291.68362]
Cohen, Ernie; Schirmer, Bert, From total store order to sequential consistency: a practical reduction theorem, 403-418 [Zbl 1291.68334]
Sozeau, Matthieu, Equations: a dependent pattern-matching compiler, 419-434 [Zbl 1291.68369]
Swords, Sol; Hunt, Warren A. jun., A mechanically verified AIG-to-BDD conversion algorithm, 435-449 [Zbl 1266.68165]
Walukiewicz-Chrząszcz, Daria; Chrząszcz, Jacek, Inductive consequences in the calculus of constructions, 450-465 [Zbl 1291.68374]
Weber, Tjark, Validating QBF invalidity in HOL4, 466-480 [Zbl 1291.68375]
Howe, Douglas J., Higher-order abstract syntax in Isabelle/HOL, 481-484 [Zbl 1291.68349]
Myreen, Magnus O., Separation logic adapted for proofs by rewriting, 485-489 [Zbl 1291.68363]
Spitters, Bas; van der Weegen, Eelis, Developing the algebraic hierarchy with type classes in Coq, 490-493 [Zbl 1291.68370]

MSC:
68-06 Proceedings, conferences, collections, etc. pertaining to computer science
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
00B25 Proceedings of conferences of miscellaneous specific interest
Software:
z3; HOL Light; HOL; Coq
PDF BibTeX XML Cite
Full Text: DOI