| Publication | Date of Publication | Type |
|---|
| Animating MRBNFs: truly modular binding-aware datatypes in Isabelle/HOL | 2026-09-01 | Paper |
| Completing structured arguments in assumption-based argumentation | 2025-12-15 | Paper |
Relative security: (dis)proving resilience against semantic optimization vulnerabilities in Isabelle/HOL. Extended version
Journal of Automated Reasoning | 2025-11-26 | Paper |
| Reasoning in assumption-based argumentation using tree-decompositions | 2024-05-29 | Paper |
| Bounded-Deducibility Security (Invited Paper) | 2023-06-20 | 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 |
| A formally verified abstract account of Gödel's incompleteness theorems | 2020-03-10 | Paper |
| Formal verification of language-based concurrent noninterference | 2019-09-18 | Paper |
A consistent foundation for Isabelle/HOL
Journal of Automated Reasoning | 2019-04-29 | Paper |
From types to sets by local type definition in higher-order logic
Journal of Automated Reasoning | 2019-02-18 | Paper |
CoSMed: a confidentiality-verified social media platform
Journal of Automated Reasoning | 2018-08-21 | Paper |
| Foundational (co)datatypes and (co)recursion for higher-order logic | 2018-01-04 | 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 |
Comprehending Isabelle/HOL’s Consistency
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 |
Encoding monomorphic and polymorphic types
Logical Methods in Computer Science | 2017-04-11 | Paper |
From types to sets by local type definitions in higher-order logic
Interactive Theorem Proving | 2016-10-27 | Paper |
CoSMed: a confidentiality-verified social media platform
Interactive Theorem Proving | 2016-10-27 | Paper |
Witnessing (co)datatypes
Programming Languages and Systems | 2016-04-26 | Paper |
A consistent foundation for Isabelle/HOL
Interactive Theorem Proving | 2015-09-14 | Paper |
Term-generic logic
Theoretical Computer Science | 2015-04-01 | Paper |
Recursion principles for syntax with bindings and substitution
Proceedings of the 16th ACM SIGPLAN international conference on Functional programming | 2015-03-05 | Paper |
Formalizing probabilistic noninterference
Certified Programs and Proofs | 2015-01-13 | Paper |
Unified Classical Logic Completeness
Automated Reasoning | 2014-09-26 | Paper |
Cardinals in Isabelle/HOL
Interactive Theorem Proving | 2014-09-08 | Paper |
Truly modular (co)datatypes for Isabelle/HOL
Interactive Theorem Proving | 2014-09-08 | Paper |
Mechanizing the metatheory of Sledgehammer
Frontiers of Combining Systems | 2013-09-20 | Paper |
Noninterfering schedulers. When possibilistic noninterference implies probabilistic noninterference
Algebra and Coalgebra in Computer Science | 2013-09-13 | Paper |
Encoding monomorphic and polymorphic types
Tools and Algorithms for the Construction and Analysis of Systems | 2013-08-05 | Paper |
Proving concurrent noninterference
Certified Programs and Proofs | 2013-04-19 | Paper |
More SPASS with Isabelle
Interactive Theorem Proving | 2012-09-20 | Paper |
Weak bisimilarity coalgebraically
Algebra and Coalgebra in Computer Science | 2012-06-01 | Paper |
Incremental pattern-based coinduction for process algebra and its Isabelle formalization
Foundations of Software Science and Computational Structures | 2010-04-27 | Paper |
Term-Generic Logic
Recent Trends in Algebraic Development Techniques | 2009-10-22 | Paper |
A semantic approach to interpolation
Theoretical Computer Science | 2009-03-25 | Paper |
| Order convergence and distance on Łukasiewicz-Moisil algebras | 2008-07-01 | Paper |
| A new class of probabilities on Łukasiewicz-Moisil algebras | 2008-02-11 | Paper |
Foundations of Software Science and Computation Structures
Lecture Notes in Computer Science | 2007-05-02 | Paper |
An institution-independent proof of the Robinson consistency theorem
Studia Logica | 2007-04-26 | Paper |
An Institution-independent Generalization of Tarski's Elementary Chain Theorem
Journal Of Logic And Computation | 2007-04-13 | Paper |
Some algebraic theory for many-valued relation algebras
Algebra Universalis | 2007-04-02 | Paper |
A common generalization for MV-algebras and Łukasiewicz-Moisil algebras
Archive for Mathematical Logic | 2007-01-24 | Paper |
Algebra and Coalgebra in Computer Science
Lecture Notes in Computer Science | 2006-10-20 | Paper |
Łukasiewicz-Moisil relation algebras
Studia Logica | 2006-03-17 | Paper |
Many-valued relation algebras
Algebra Universalis | 2006-01-06 | Paper |
Similarity Convergence in Residuated Structures
Logic Journal of the IGPL | 2005-11-08 | Paper |
| scientific article; zbMATH DE number 2172904 (Why is no real title available?) | 2005-06-07 | Paper |
Non-dual fuzzy connections
Archive for Mathematical Logic | 2005-02-11 | Paper |
A general approach to fuzzy concepts
Mathematical Logic Quarterly | 2004-08-06 | Paper |
Non-commutative fuzzy structures and pairs of weak negations.
Fuzzy Sets and Systems | 2004-03-29 | Paper |
| scientific article; zbMATH DE number 1876861 (Why is no real title available?) | 2003-11-12 | Paper |
Non-commutative fuzzy Galois connections
Soft Computing | 2003-08-31 | Paper |
