Theoretical Computer Science

Research Output 1993 2019

2019

A formal proof of Hensel's lemma over the p-adic integers

Lewis, R. Y., 14 Jan 2019, CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019. Mahboubi, A. (ed.). Association for Computing Machinery, Inc, p. 15-26 12 p.

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

Number theory
Polynomials

A Formal Proof of the Expressiveness of Deep Learning

Bentkamp, A., Blanchette, J. C. & Klakow, D., Aug 2019, In : Journal of Automated Reasoning. 63, 2, p. 347-368

Research output: Contribution to JournalArticleAcademicpeer-review

A verified prover based on ordered resolution

Schlichtkrull, A., Blanchette, J. C. & Traytel, D., 14 Jan 2019, CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019. Mahboubi, A. (ed.). Association for Computing Machinery, Inc, p. 152-165 14 p.

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

Specifications

Extending a brainiac prover to lambda-free higher-order logic

Vukmirović, P., Blanchette, J. C., Cruanes, S. & Schulz, S., 2019, Tools and Algorithms for the Construction and Analysis of Systems: 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings - Part 1. Zhang, L. & Vojnar, T. (eds.). Springer Verlag, Vol. 1. p. 192-210 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 11427 LNCS).

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

Higher-order Logic
Data structures
Algorithms and Data Structures
Higher Order
Theorem proving

Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk)

Blanchette, J. C., 14 Jan 2019, CPP 2019 - Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2019. Mahboubi, A. (ed.). Association for Computing Machinery, Inc, p. 1-13 13 p.

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

Genome-wide meta-analysis identifies new loci and functional pathways influencing Alzheimer's disease risk

Jansen, I. E., Savage, J. E., Watanabe, K., Bryois, J., Williams, D. M., Steinberg, S., Sealock, J., Karlsson, I. K., Hägg, S., Athanasiu, L., Voyle, N., Proitsi, P., Witoelar, A., Stringer, S., Aarsland, D., Almdahl, I. S., Andersen, F., Bergh, S., Bettella, F., Bjornsson, S. & 33 othersBrækhus, A., Bråthen, G., de Leeuw, C., Desikan, R. S., Djurovic, S., Dumitrescu, L., Fladby, T., Hohman, T. J., Jonsson, P. V., Kiddle, S. J., Rongve, A., Saltvedt, I., Sando, S. B., Selbæk, G., Shoai, M., Skene, N. G., Snaedal, J., Stordal, E., Ulstein, I. D., Wang, Y., White, L. R., Hardy, J., Hjerling-Leffler, J., Sullivan, P. F., van der Flier, W. M., Dobson, R., Davis, L. K., Stefansson, H., Stefansson, K., Pedersen, N. L., Ripke, S., Andreassen, O. A. & Posthuma, D., Mar 2019, In : Nature Genetics. 51, 3, p. 404-413 10 p.

Research output: Contribution to JournalArticleAcademicpeer-review

Open Access
File
Meta-Analysis
Alzheimer Disease
Genome
Proxy
Genes

L.E.J. Brouwer, fifty years later

van Dalen, D., Jongbloed, G., Klop, J. W. & van Mill, J., 11 Jan 2019, (Accepted/In press) In : Indagationes Mathematicae. p. 1-16 16 p.

Research output: Contribution to JournalArticleAcademicpeer-review

Projections for infinitary rewriting (extended version)

Lombardi, C., Ríos, A. & de Vrijer, R., 16 Aug 2019, In : Theoretical Computer Science. 781, p. 92-110 19 p.

Research output: Contribution to JournalArticleAcademicpeer-review

Rewriting
Projection
Term Rewriting
Term
Contraction

Reliable Restricted Process Theory

Ghassemi, F. & Fokkink, W., 14 Feb 2019, In : Fundamenta Informaticae. 165, 1, p. 1-41 41 p.

Research output: Contribution to JournalArticleAcademicpeer-review

Communication
Network protocols
Network Protocols
Axiomatization
Multi-hop

Scalable Fine-Grained Proofs for Formula Processing

Barbosa, H., Blanchette, J. C., Fleury, M. & Fontaine, P., 4 Jan 2019, In : Journal of Automated Reasoning. p. 1-26 26 p.

Research output: Contribution to JournalArticleAcademicpeer-review

Surface mount technology
Data structures
Processing

Selected Extended Papers of ITP 2016: Preface

Blanchette, J. C. & Merz, S., Feb 2019, In : Journal of Automated Reasoning. 62, 2, p. 169-170 2 p.

Research output: Contribution to JournalEditorialAcademicpeer-review

Superposition with Lambdas

Bentkamp, A., Blanchette, J. C., Tourret, S., Vukmirovic, P. & Waldmann, U., 19 Apr 2019, (Accepted/In press) The 27th International Conference on Automated Deduction: CADE-27.

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

Equivalence classes

Syllogistic logic with Most

Endrullis, J. & Moss, L. S., 1 Jun 2019, In : Mathematical Structures in Computer Science. 29, 6, p. 763-782 20 p.

Research output: Contribution to JournalArticleAcademicpeer-review

Computability and decidability
Polynomials
Logic
Soundness
Decidability
Multiple Sequence Alignment
Workflow
Sequence Alignment
Work Flow
Alignment
2018

A Formal Proof of the Expressiveness of Deep Learning

Bentkamp, A., Blanchette, J. C. & Klakow, D., 22 Sep 2018, (Accepted/In press) In : Journal of Automated Reasoning. p. 1-22 22 p.

Research output: Contribution to JournalArticleAcademicpeer-review

Open Access
Image recognition
Bioinformatics
Computer science
Tensors
Polynomials

A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality

Blanchette, J. C., Fleury, M., Lammich, P. & Weidenbach, C., 12 Mar 2018, In : Journal of Automated Reasoning. 2018, p. 1-33 33 p.

Research output: Contribution to JournalArticleAcademicpeer-review

Open Access
Functional programming
Computer programming languages
Data structures
Concretes
Experiments

A verified SAT solver with watched literals using Imperative HOL

Fleury, M., Blanchette, J. C. & Lammich, P., Jan 2018, CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018. New York, NY: Association for Computing Machinery, Inc, p. 158-171 14 p.

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

Data structures

Braids via term rewriting

Endrullis, J. & Klop, J. W., 6 Dec 2018, In : Theoretical Computer Science. p. 1-36 36 p.

Research output: Contribution to JournalArticleAcademicpeer-review

Term Rewriting
Braid
Notation
Diamonds
Diagram

Coinductive foundations of infinitary rewriting and infinitary equational logic

Endrullis, J., Hansen, H. H., Hendriks, D., Polonsky, A. & Silva, A., 10 Jan 2018, In : Logical Methods in Computer Science. 14, 1, p. 1-44 44 p., 3.

Research output: Contribution to JournalArticleAcademicpeer-review

Open Access
Infinitary Logic
Equational Logic
Rewriting
Term Rewriting
Equational Theory

Decreasing diagrams with two labels are complete for confluence of countable systems

Endrullis, J., Klop, J. W. & Overbeek, R., 1 Jul 2018, 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Vol. 108. p. 1-15 15 p. 14

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

Labels
Electric commutation
Labeling

Degrees of Infinite Words, Polynomials and Atoms

Endrullis, J., Karhumäki, J., Klop, J. W. & Saarela, A., Aug 2018, In : International Journal of Foundations of Computer Science. 29, 5, p. 825-843 19 p.

Research output: Contribution to JournalArticleAcademicpeer-review

Transducers
Polynomials
Atoms
Turing machines
Equivalence classes

Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover

Schlichtkrull, A., Blanchette, J. C., Traytel, D. & Waldmann, U., 2018, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer/Verlag, p. 89-107 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10900 LNAI).

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

Theorem proving
Automated Reasoning
Formal Proof
Theorem Proving
Formalization

Formal Modeling and Analysis of Mobile Ad hoc Networks

Ghassemi Esfahani, F., 2018, 232 p.

Research output: PhD ThesisPhD Thesis - Research VU, graduation VUAcademic

Open Access
File

Introduction to Milestones in Interactive Theorem Proving

Avigad, J., Blanchette, J. C., Klein, G., Paulson, L., Popescu, A. & Snelting, G., Jun 2018, In : Journal of Automated Reasoning. 61, 1-4, p. 1-8 8 p.

Research output: Contribution to JournalEditorialAcademicpeer-review

Introduction to the STAF 2015 special section

Blanchette, J., Bordeleau, F., Pierantonio, A., Kosmatov, N., Taentzer, G. & Wimmer, M., 7 Jul 2018, (Accepted/In press) In : Software and Systems Modeling. p. 1-3 3 p.

Research output: Contribution to JournalArticleAcademicpeer-review

MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)

Wimmer, S. & Hölzl, J., 2018, Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer/Verlag, p. 597-603 7 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 contributionAcademicpeer-review

Probabilistic Automata
Timed Automata
Markov Decision Process
Model checking
Formalization

Motif-Aware PRALINE: Improving the alignment of motif regions: Improving the alignment of motif regions

Dijkstra, M., Bawono, P., Abeln, S., Feenstra, K. A., Fokkink, W. & Heringa, J., 1 Nov 2018, In : PLoS Computational Biology. 14, 11, p. 1-19 19 p., e1006547.

Research output: Contribution to JournalArticleAcademicpeer-review

Open Access
Sequence Alignment
sequence alignment
Alignment
Multiple Sequence Alignment
Benchmarking

SOS-based modal decomposition on nondeterministic probabilistic processes

Castiglioni, V., Gebler, D. & Tini, S., 25 Jun 2018, In : Logical Methods in Computer Science. 14, 2, p. 1-51 51 p., 18.

Research output: Contribution to JournalArticleAcademicpeer-review

Open Access
Decomposition
Decompose
Structural Operational Semantics
Nondeterminism
Congruence

SOS specifications for uniformly continuous operators

Gebler, D. & Tini, S., Mar 2018, In : Journal of Computer and System Sciences. 92, March, p. 113-151 39 p.

Research output: Contribution to JournalArticleAcademicpeer-review

Uniformly continuous
Semantics
Specification
Specifications
Operator

Superposition for Lambda-Free Higher-Order Logic

Bentkamp, A., Blanchette, J. C., Cruanes, S. & Waldmann, U., 2018, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer/Verlag, p. 28-46 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10900 LNAI).

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

Higher-order Logic
Superposition
Calculus
Monotonic
Higher Order

The characteristics of molten globule states and folding pathways strongly depend on the sequence of a protein

Dijkstra, M. J. J., Fokkink, W. J., Heringa, J., van Dijk, E. & Abeln, S., 17 Nov 2018, In : Molecular Physics. 116, 21-22, p. 3173-3180 8 p.

Research output: Contribution to JournalArticleAcademicpeer-review

Open Access
globules
folding
Molten materials
Hot Temperature
proteins
2017

A formal proof of the expressiveness of deep learning

Bentkamp, A., Blanchette, J. C. & Klakow, D., 2017, Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasilia, Brazil, September 26-29, 2017, Proceedings. Springer, Vol. 10499. p. 46-64 (LNCS).

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

Image recognition
Bioinformatics
Computer science
Tensors
Polynomials

A lambda-free higher-order recursive path order

Blanchette, J. C., Waldmann, U. & Wand, D., 1 Jan 2017, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings. Esparza, J. & Murawski, A. S. (eds.). Springer/Verlag, p. 461-479 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10203 LNCS).

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

Substitution reactions
Higher Order
Path
Transitivity
Term

An Isabelle Formalization of the Expressiveness of Deep Learning (Extended Abstract)

Bentkamp, A., Blanchette, J. C. & Klakow, D., 2017, p. 22-23. 2 p.

Research output: Contribution to ConferenceAbstractOther research output

Substitution reactions
Higher Order
Term
Transitivity
Compatibility

A transfinite knuth–bendix order for lambda-free higher-order terms

Becker, H., Blanchette, J. C., Waldmann, U. & Wand, D., 2017, Automated Deduction - CADE 26: 26th International Conference on Automated Deduction, Proceedings. de Moura, L. (ed.). Springer/Verlag, p. 432-453 22 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10395 LNAI).

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

Substitution reactions
Higher Order
Term
Transitivity
Compatibility

A verified SAT solver framework with learn, forget, restart, and incrementality

Blanchette, J. C., Fleury, M. & Weidenbach, C., 1 Jan 2017, 26th International Joint Conference on Artificial Intelligence, IJCAI 2017. Sierra, C. (ed.). International Joint Conferences on Artificial Intelligence, AAAI Press, p. 4786-4790 5 p.

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

Experiments

Clocked lambda calculus

Endrullis, J., Hendriks, D., Klop, J. W. & Polonsky, A., 1 Jun 2017, In : Mathematical Structures in Computer Science (MSCS). 27, 5, p. 782-806 25 p.

Research output: Contribution to JournalArticleAcademicpeer-review

Lambda Calculus
Calculus
Term
Normal Form
Fixed point

Creating Büchi automata for multi-valued model checking

Vijzelaar, S. J. J. & Fokkink, W. J., 2017, Formal Techniques for Distributed Objects, Components, and Systems - 37th IFIP WG 6.1 International Conference, FORTE 2017 Held as Part of the 12th International Federated Conference on Distributed Computing Techniques, DisCoTec 2017, Proceedings. Springer/Verlag, Vol. 10321 LNCS. p. 210-224 15 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10321 LNCS).

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

Model checking
Model Checking
Automata
Logic
Kripke Models

Detecting useless transitions in pushdown automata

Grune, D., Fokkink, W., Chatzikalymnios, E., Hond, B. & Rutgers, P., 2017, Language and Automata Theory and Applications - 11th International Conference, LATA 2017, Proceedings. Springer/Verlag, Vol. 10168 LNCS. p. 421-434 14 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10168 LNCS).

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

Pushdown Automata
Finite automata
Finite Automata
Automata

Divide and congruence II: From decomposition of modal formulas to preservation of delay and weak bisimilarity

Fokkink, W. & van Glabbeek, R., 1 Dec 2017, In : Information and Computation. 257, p. 79-113 35 p.

Research output: Contribution to JournalArticleAcademicpeer-review

Preservation
Congruence
Divides
Decomposition Method
Decomposition

Divide and congruence III: Stability & divergence

Fokkink, W., Glabbeek, R. V. & Luttik, B., 1 Aug 2017, 28th International Conference on Concurrency Theory, CONCUR 2017. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Vol. 85. 15

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

Semantics
Decomposition

Foundational (co)datatypes and (co)recursion for higher-order logic

Biendarra, J., Blanchette, J. C., Bouzy, A., Desharnais, M., Fleury, M., Hölzl, J., Kunčar, O., Lochbihler, A., Meier, F., Panny, L., Popescu, A., Sternagel, C., Thiemann, R. & Traytel, D., 1 Jan 2017, Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Proceedings. Dixon, C. & Finger, M. (eds.). Springer/Verlag, p. 3-21 19 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10483 LNAI).

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

Recursive functions
Higher-order Logic
Recursion
Coinduction
Recursive Functions

Foundational nonuniform (Co)datatypes for higher-order logic

Blanchette, J. C., Meier, F., Popescu, A. & Traytel, D., 8 Aug 2017, 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017. Institute of Electrical and Electronics Engineers Inc., 8005071

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

Higher-order Logic
Specification languages
Data structures
Coinduction
Functional Data

Friends with benefits: Implementing corecursion in foundational proof assistants

Blanchette, J. C., Bouzy, A., Lochbihler, A., Popescu, A. & Traytel, D., 1 Jan 2017, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings. Yang, H. (ed.). Springer/Verlag, p. 111-140 30 p. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); vol. 10201 LNCS).

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

Productivity
Specifications
Inconsistency
Registration
Synthesis

Language and Proofs for Higher-Order SMT (Work in Progress)

Barbosa, H., Blanchette, J. C., Cruanes, S., El Ouraoui, D. & Fontaine, P., 2017, In : Electronic Proceedings in Theoretical Computer Science. 262, p. 15-22

Research output: Contribution to JournalArticleAcademicpeer-review

Open Access

Maximally permissive controlled system synthesis for non-determinism and modal logic

van Hulst, A. C., Reniers, M. A. & Fokkink, W. J., 1 Mar 2017, In : Discrete Event Dynamic Systems. 27, 1, p. 109-142 34 p.

Research output: Contribution to JournalArticleAcademicpeer-review

Open Access
Nondeterminism
Modal Logic
Synthesis
Supervisory Control
Requirements

Model-based design of supervisory controllers for baggage handling systems

Swartjes, L., van Beek, D. A., Fokkink, W. J. & van Eekelen, J. A. W. M., 1 Nov 2017, In : Simulation Modelling Practice and Theory. 78, p. 28-50 23 p.

Research output: Contribution to JournalArticleAcademicpeer-review

Baggage handling
Model-based Design
Controller
Controllers
Formal Model

Multi-valued simulation and abstraction using lattice operations

Vijzelaar, S. & Fokkink, W. J., 1 Jan 2017, In : ACM Transactions on Embedded Computing Systems. 16, 2, 42.

Research output: Contribution to JournalArticleAcademicpeer-review

Nested multisets, hereditary multisets, & syntactic ordinals in Isabelle/HOL

Blanchette, J. C., Fleury, M. & Traytel, D., 1 Sep 2017, 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017. Miller, D. (ed.). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Vol. 84. 11

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

Syntactics
Computability and decidability