Filter
Conference contribution

Search results

  • 2024

    Alpha-Beta Pruning Verified

    Nipkow, T., Sep 2024, 15th International Conference on Interactive Theorem Proving, ITP 2024. Bertot, Y., Kutsia, T. & Norrish, M. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 1. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 309).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • A Verified Earley Parser

    Rau, M. & Nipkow, T., Sep 2024, 15th International Conference on Interactive Theorem Proving, ITP 2024. Bertot, Y., Kutsia, T. & Norrish, M. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 31. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 309).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • 2023

    Real-Time Double-Ended Queue Verified (Proof Pearl)

    Toth, B. & Nipkow, T., Jul 2023, 14th International Conference on Interactive Theorem Proving, ITP 2023. Naumowicz, A. & Thiemann, R. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 29. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 268).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • Verification of NP-Hardness Reduction Functions for Exact Lattice Problems

    Kreuzer, K. & Nipkow, T., 2023, Automated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings. Pientka, B. & Tinelli, C. (eds.). Springer Science and Business Media Deutschland GmbH, p. 365-381 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 14132 LNAI).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    2 Scopus citations
  • 2022

    A Verified Implementation of B + -Trees in Isabelle/HOL

    Mündler, N. & Nipkow, T., 2022, Theoretical Aspects of Computing – ICTAC 2022 - 19th International Colloquium, Proceedings. Seidl, H., Liu, Z. & Pasareanu, C. S. (eds.). Springer Science and Business Media Deutschland GmbH, p. 324-341 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 13572 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
  • 2021

    A Verified Decision Procedure for Orders in Isabelle/HOL

    Stevens, L. & Nipkow, T., 2021, Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Proceedings. Hou, Z. & Ganesh, V. (eds.). Springer Science and Business Media Deutschland GmbH, p. 127-143 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12971 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    1 Scopus citations
  • Isabelle’s Metalogic: Formalization and Proof Checker

    Nipkow, T. & Roßkopf, S., 2021, Automated Deduction – CADE 28 - 28th International Conference on Automated Deduction, 2021, Proceedings. Platzer, A. & Sutcliffe, G. (eds.). Springer Science and Business Media Deutschland GmbH, p. 93-110 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12699 LNAI).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    9 Scopus citations
  • Teaching algorithms and data structures with a proof assistant (invited talk)

    Nipkow, T., 17 Jan 2021, CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021. Hritcu, C. & Popescu, A. (eds.). Association for Computing Machinery, Inc, p. 1-3 3 p. (CPP 2021 - Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2021).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    2 Scopus citations
  • 2020

    Proof pearl: Braun trees

    Nipkow, T. & Sewell, T., 20 Jan 2020, CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020. Blanchette, J. & Hritcu, C. (eds.). Association for Computing Machinery, Inc, p. 18-31 14 p. (CPP 2020 - Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2020).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    1 Scopus citations
  • Verification of Closest Pair of Points Algorithms

    Rau, M. & Nipkow, T., 2020, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Proceedings. Peltier, N. & Sofronie-Stokkermans, V. (eds.). Springer, p. 341-357 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12167 LNAI).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    1 Scopus citations
  • Verified Approximation Algorithms

    Eßmann, R., Nipkow, T. & Robillard, S., 2020, Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Proceedings. Peltier, N. & Sofronie-Stokkermans, V. (eds.). Springer, p. 291-306 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12167 LNAI).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    3 Scopus citations
  • Verified Textbook Algorithms: A Biased Survey

    Nipkow, T., Eberl, M. & Haslbeck, M. P. L., 2020, Automated Technology for Verification and Analysis - 18th International Symposium, ATVA 2020, Proceedings. Hung, D. V. & Sokolsky, O. (eds.). Springer Science and Business Media Deutschland GmbH, p. 25-53 29 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 12302 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    8 Scopus citations
  • 2019

    Proof pearl: Purely functional, simple and efficient priority search trees and applications to Prim and Dijkstra

    Lammich, P. & Nipkow, T., Sep 2019, 10th International Conference on Interactive Theorem Proving, ITP 2019. Harrison, J., O'Leary, J. & Tolmach, A. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 23. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 141).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    3 Scopus citations
  • Trustworthy graph algorithms

    Abdulaziz, M., Mehlhorn, K. & Nipkow, T., Aug 2019, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019. Katoen, J.-P., Heggernes, P. & Rossmanith, P. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 1. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 138).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    5 Scopus citations
  • 2018

    A verified compiler from isabelle/HOL to CakeML

    Hupel, L. & Nipkow, T., 2018, Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Ahmed, A. (ed.). Springer Verlag, p. 999-1026 28 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10801 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    26 Scopus citations
  • Hoare logics for time bounds: A study in meta theory

    Haslbeck, M. P. L. & Nipkow, T., 2018, Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings. Beyer, D. & Huisman, M. (eds.). Springer Verlag, p. 155-171 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10805 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    11 Scopus citations
  • Verified Analysis of Random Binary Tree Structures

    Eberl, M., Haslbeck, M. W. & Nipkow, T., 2018, Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Avigad, J. & Mahboubi, A. (eds.). Springer Verlag, p. 196-214 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10895 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    4 Scopus citations
  • Verified Memoization and Dynamic Programming

    Wimmer, S., Hu, S. & Nipkow, T., 2018, Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Avigad, J. & Mahboubi, A. (eds.). Springer Verlag, p. 579-596 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10895 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    5 Scopus citations
  • 2017

    Formalising and monitoring traffic rules for autonomous vehicles in Isabelle/HOL

    Rizaldi, A., Keinholz, J., Huber, M., Feldle, J., Immler, F., Althoff, M., Hilgendorf, E. & Nipkow, T., 2017, Integrated Formal Methods - 13th International Conference, IFM 2017, Proceedings. Schneider, S. & Polikarpova, N. (eds.). Springer Verlag, p. 50-66 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10510 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    64 Scopus citations
  • Formalized Proof Systems for Propositional Logic

    Michaelis, J. & Nipkow, T., 2017, 23rd International Conference on Types for Proofs and Programs, TYPES 2017. Kaposi, A. (ed.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 5. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 104).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    12 Scopus citations
  • Verified root-balanced trees

    Nipkow, T., 2017, Programming Languages and Systems - 15th Asian Symposium, APLAS 2017, Proceedings. Chang, B.-Y. E. (ed.). Springer Verlag, p. 255-272 18 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10695 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    9 Scopus citations
  • 2016

    Automatic functional correctness proofs for functional search trees

    Nipkow, T., 2016, Interactive Theorem Proving - 7th International Conference, ITP 2016, Proceedings. Blanchette, J. C. & Merz, S. (eds.). Springer Verlag, p. 307-322 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9807 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    10 Scopus citations
  • Verified Analysis of Functional Data Structures

    Nipkow, T., 1 Jun 2016, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016. Kesner, D. & Pientka, B. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 4. (Leibniz International Proceedings in Informatics, LIPIcs; vol. 52).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    2 Scopus citations
  • Verified analysis of list update algorithms

    Haslbeck, M. P. L. & Nipkow, T., 1 Dec 2016, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2016. Lal, A., Akshay, S., Saurabh, S., Sen, S. & Saurabh, S. (eds.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, p. 49.1-49.15 (Leibniz International Proceedings in Informatics, LIPIcs; vol. 65).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    1 Scopus citations
  • 2015

    Amortized complexity verified

    Nipkow, T., 2015, Interactive Theorem Proving - 6th International Conference, ITP 2015, Proceedings. Zhang, X. & Urban, C. (eds.). Springer Verlag, p. 310-324 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9236).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    19 Scopus citations
  • A verified compiler for probability density functions

    Eberl, M., Hölzl, J. & Nipkow, T., 2015, Programming Languages and Systems - 24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings. Vitek, J. (ed.). Springer Verlag, p. 80-104 25 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9032).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    20 Scopus citations
  • Mining the archive of formal proofs

    Blanchette, J. C., Haslbeck, M., Matichuk, D. & Nipkow, T., 2015, Intelligent Computer Mathematics - International Conference, CICM 2015, Proceedings. Kerber, M., Sorge, V., Rabe, F., Carette, J. & Kaliszyk, C. (eds.). Springer Verlag, p. 3-17 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 9150).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    31 Scopus citations
  • 2014

    Experience report: The next 1100 Haskell programmers

    Blanchette, J. C., Hupel, L., Nipkow, T., Noschinski, L. & Traytel, D., 2014, Haskell 2014 - Proceedings of the 2014 ACM SIGPLAN Haskell Symposium. Association for Computing Machinery, p. 25-30 6 p. (Haskell 2014 - Proceedings of the 2014 ACM SIGPLAN Haskell Symposium).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • Unified decision procedures for regular expression equivalence

    Nipkow, T. & Traytel, D., 2014, Interactive Theorem Proving - 5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Proceedings. Springer Verlag, p. 450-466 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8558 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    17 Scopus citations
  • 2013

    A brief survey of verified decision procedures for equivalence of regular expressions

    Nipkow, T. & Haslbeck, M., 2013, Automated Reasoning with Analytic Tableaux and Related Methods - 22nd International Conference, TABLEAUX 2013, Proceedings. p. 10-12 3 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8123 LNAI).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

  • A fully verified executable LTL model checker

    Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A. & Smaus, J. G., 2013, Computer Aided Verification - 25th International Conference, CAV 2013, Proceedings. p. 463-478 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8044 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    72 Scopus citations
  • Data refinement in Isabelle/HOL

    Haftmann, F., Krauss, A., Kunčar, O. & Nipkow, T., 2013, Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings. p. 100-115 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7998 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    49 Scopus citations
  • Formalizing probabilistic noninterference

    Popescu, A., Hol̈zl, J. & Nipkow, T., 2013, Certified Programs and Proofs - Third International Conference, CPP 2013, Proceedings. p. 259-275 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8307 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    9 Scopus citations
  • Noninterfering schedulers when possibilistic noninterference implies probabilistic noninterference

    Popescu, A., Hölzl, J. & Nipkow, T., 2013, Algebra and Coalgebra in Computer Science - 5th International Conference, CALCO 2013, Proceedings. Springer Verlag, p. 236-252 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 8089 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    5 Scopus citations
  • Verified decision procedures for MSO on words based on derivatives of regular expressions

    Traytel, D. & Nipkow, T., 2013, ICFP 2013 - Proceedings of the 2013 ACM SIGPLAN International Conference on Functional Programming. p. 3-12 10 p. (Proceedings of the ACM SIGPLAN International Conference on Functional Programming, ICFP).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    4 Scopus citations
  • 2012

    Abstract interpretation of annotated commands

    Nipkow, T., 2012, Interactive Theorem Proving - Third International Conference, ITP 2012, Proceedings. p. 116-132 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7406 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    10 Scopus citations
  • Proving concurrent noninterference

    Popescu, A., Hölzl, J. & Nipkow, T., 2012, Certified Programs and Proofs - Second International Conference, CPP 2012, Proceedings. p. 109-125 17 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7679 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    9 Scopus citations
  • Teaching semantics with a proof assistant: No more LSD trip proofs

    Nipkow, T., 2012, Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings. p. 24-38 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7148 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    23 Scopus citations
  • Verifying pCTL model checking

    Hölzl, J. & Nipkow, T., 2012, Tools and Algorithms for the Construction and Analysis of Systems - 18th Int. Conf., TACAS 2012, Held as Part of the European Joint Conf. on Theory and Practice of Software, ETAPS 2012, Proceedings. p. 347-361 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7214 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    5 Scopus citations
  • 2011

    Automatic proof and disproof in Isabelle/HOL

    Blanchette, J. C., Bulwahn, L. & Nipkow, T., 2011, Frontiers of Combining Systems - 8th International Symposium, FroCoS 2011, Proceedings. p. 12-27 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6989 LNAI).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    70 Scopus citations
  • Extending hindley-milner type inference with coercive structural subtyping

    Traytel, D., Berghofer, S. & Nipkow, T., 2011, Programming Languages and Systems - 9th Asian Symposium, APLAS 2011, Proceedings. p. 89-104 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7078 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    12 Scopus citations
  • Proof pearl: The marriage theorem

    Jiang, D. & Nipkow, T., 2011, Certified Programs and Proofs - First International Conference, CPP 2011, Proceedings. p. 394-399 6 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 7086 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    1 Scopus citations
  • Verified efficient enumeration of plane graphs modulo isomorphism

    Nipkow, T., 2011, Interactive Theorem Proving - Second International Conference, ITP 2011, Proceedings. p. 281-296 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6898 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    7 Scopus citations
  • 2010

    Code generation via higher-order rewrite systems

    Haftmann, F. & Nipkow, T., 2010, Functional and Logic Programming - 10th International Symposium, FLOPS 2010, Proceedings. p. 103-117 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6009 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Open Access
    137 Scopus citations
  • Nitpick: A counterexample generator for higher-order logic based on a relational model finder

    Blanchette, J. C. & Nipkow, T., 2010, Interactive Theorem Proving - First International Conference, ITP 2010, Proceedings. p. 131-146 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6172 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    163 Scopus citations
  • Sledgehammer: Judgement day

    Böhme, S. & Nipkow, T., 2010, Automated Reasoning - 5th International Joint Conference, IJCAR 2010, Proceedings. p. 107-121 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 6173 LNAI).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    82 Scopus citations
  • 2008

    A compiled implementation of normalization by evaluation

    Aehlig, K., Haftmann, F. & Nipkow, T., 2008, Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings. Springer Verlag, p. 39-54 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 5170 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    9 Scopus citations
  • Linear quantifier elimination

    Nipkow, T., 2008, Automated Reasoning - 4th International Joint Conference, IJCAR 2008, Proceedings. p. 18-33 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 5195 LNAI).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    16 Scopus citations
  • The isabelle framework

    Wenzel, M., Paulson, L. C. & Nipkow, T., 2008, Theorem Proving in Higher Order Logics - 21st International Conference, TPHOLs 2008, Proceedings. Springer Verlag, p. 33-38 6 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 5170 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    104 Scopus citations
  • 2007

    Finding lexicographic orders for termination proofs in Isabelle/HOL

    Bulwahn, L., Krauss, A. & Nipkow, T., 2007, Theorem Proving in Higher Order Logics - 20th International Conference, TPHOLs 2007, Proceedings. Springer Verlag, p. 38-53 16 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 4732 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    20 Scopus citations