| Publication | Date of Publication | Type |
|---|
| Practical relational calculus query evaluation | 2024-04-25 | Paper |
| Practical relational calculus query evaluation | 2024-04-23 | Paper |
| Explainable online monitoring of metric temporal logic | 2024-04-05 | Paper |
| Verified first-order monitoring with recursive rules | 2024-02-01 | Paper |
Efficient Evaluation of Arbitrary Relational Calculus Queries
Logical Methods in Computer Science | 2024-01-16 | Paper |
Optimal proofs for linear temporal logic on lasso words
Automated Technology for Verification and Analysis | 2023-07-28 | Paper |
VeriMon: a formally verified monitoring tool
Lecture Notes in Computer Science | 2023-07-28 | Paper |
| scientific article; zbMATH DE number 7699427 (Why is no real title available?) | 2023-06-20 | Paper |
| Generic Authenticated Data Structures, Formally. | 2023-02-03 | Paper |
Multi-head Monitoring of Metric Dynamic Logic
1517.6825 | 2022-12-22 | Paper |
| A formally verified, optimized monitor for metric first-order dynamic logic | 2022-11-09 | Paper |
Quotients of Bounded Natural Functors
Automated Reasoning | 2022-11-09 | Paper |
| From Nondeterministic to Multi-Head Deterministic Finite-State Transducers | 2022-07-21 | Paper |
scientific article; zbMATH DE number 7471712 (Why is no real title available?)
(available as arXiv preprint) | 2022-02-09 | Paper |
| scientific article; zbMATH DE number 7471712 (Why is no real title available?) | 2022-02-09 | Paper |
Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
Journal of Automated Reasoning | 2021-11-24 | Paper |
| Foundational nonuniform (co)datatypes for higher-order logic | 2021-01-19 | Paper |
Formalizing Bachmair and Ganzinger's ordered resolution prover
Journal of Automated Reasoning | 2020-11-02 | Paper |
Almost event-rate independent monitoring of metric temporal logic
Tools and Algorithms for the Construction and Analysis of Systems | 2020-08-05 | Paper |
Multi-head monitoring of metric temporal logic
Automated Technology for Verification and Analysis | 2020-07-20 | Paper |
Adaptive online first-order monitoring
Automated Technology for Verification and Analysis | 2020-07-20 | Paper |
| scientific article; zbMATH DE number 7204430 (Why is no real title available?) | 2020-05-26 | Paper |
| A formally verified abstract account of Gödel's incompleteness theorems | 2020-03-10 | Paper |
A survey of challenges for runtime verification from advanced application domains (beyond software)
Formal Methods in System Design | 2019-11-25 | Paper |
Almost event-rate independent monitoring
Formal Methods in System Design | 2019-11-25 | Paper |
Formalizing Bachmair and Ganzinger's ordered resolution prover
Automated Reasoning | 2018-10-18 | Paper |
| Foundational (co)datatypes and (co)recursion for higher-order logic | 2018-01-04 | Paper |
Verified decision procedures for MSO on words based on derivatives of regular expressions
Journal of Functional Programming | 2017-10-23 | Paper |
Formal Languages, Formally and Coinductively
(available as arXiv preprint) | 2017-10-17 | Paper |
scientific article; zbMATH DE number 6790165 (Why is no real title available?)
(available as arXiv preprint) | 2017-10-12 | Paper |
| A coalgebraic decision procedure for WS1S | 2017-08-31 | Paper |
Soundness and completeness proofs by coinductive methods
Journal of Automated Reasoning | 2017-07-10 | Paper |
Friends with benefits. Implementing corecursion in foundational proof assistants
Programming Languages and Systems | 2017-05-19 | Paper |
Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
2012 27th Annual IEEE Symposium on Logic in Computer Science | 2017-05-16 | Paper |
Foundational extensible corecursion: a proof assistant perspective
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming | 2017-05-10 | Paper |
Foundational extensible corecursion: a proof assistant perspective
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming | 2017-05-10 | Paper |
Witnessing (co)datatypes
Programming Languages and Systems | 2016-04-26 | Paper |
A formalized hierarchy of probabilistic system types. Proof pearl
Interactive Theorem Proving | 2015-09-14 | Paper |
Verified decision procedures for MSO on words based on derivatives of regular expressions
Proceedings of the 18th ACM SIGPLAN international conference on Functional programming | 2015-03-30 | Paper |
Unified Classical Logic Completeness
Automated Reasoning | 2014-09-26 | Paper |
Unified decision procedures for regular expression equivalence
Interactive Theorem Proving | 2014-09-08 | Paper |
Truly modular (co)datatypes for Isabelle/HOL
Interactive Theorem Proving | 2014-09-08 | Paper |
Cardinals in Isabelle/HOL
Interactive Theorem Proving | 2014-09-08 | Paper |
