| Publication | Date of Publication | Type |
|---|
| A cyclic proof system for HFL\(_\mathbb{N}\) | 2026-03-23 | Paper |
| Size-preserving translations from order-(n+1) word grammars to order-n tree grammars | 2026-02-24 | Paper |
| On average-case hardness of higher-order model checking | 2026-02-24 | Paper |
| A probabilistic higher-order fixpoint logic | 2026-02-24 | Paper |
| On the relationship between Dijkstra monads and higher-order fixpoint logic | 2025-12-04 | Paper |
Towards neural-network-guided program synthesis and verification
Formal Methods in System Design | 2025-11-07 | Paper |
| On the termination problem for probabilistic higher-order recursive programs | 2024-12-19 | Paper |
| An overview of the HFL model checking project | 2024-12-03 | Paper |
| Temporal verification of programs via first-order fixpoint logic | 2024-04-19 | Paper |
| A temporal logic for higher-order functional programs | 2024-04-19 | Paper |
| A type-based HFL model checking algorithm | 2024-04-19 | Paper |
| Neural network-guided synthesis of recursive list functions | 2023-12-13 | Paper |
| Gradual tensor shape checking | 2023-11-24 | Paper |
scientific article; zbMATH DE number 7730636 (Why is no real title available?)
(available as arXiv preprint) | 2023-08-21 | Paper |
Automated synthesis of functional programs with auxiliary functions
Programming Languages and Systems | 2023-08-02 | Paper |
HoIce: an ICE-based non-linear Horn clause solver
Programming Languages and Systems | 2023-08-02 | Paper |
Parameterized recursive refinement types for automated program verification
Static Analysis | 2023-07-28 | Paper |
On higher-order reachability games vs may reachability
Lecture Notes in Computer Science | 2023-07-21 | Paper |
| Termination Analysis for the \pi -Calculus by Reduction to Sequential Program Termination | 2023-03-29 | Paper |
RustHorn: CHC-based verification for Rust programs
Programming Languages and Systems | 2022-10-13 | Paper |
ConSORT: context- and flow-sensitive ownership refinement types for imperative programs
Programming Languages and Systems | 2022-10-13 | Paper |
| Asynchronous unfold/fold transformation for fixpoint logic | 2022-08-10 | Paper |
| Lambda-Definable Order-3 Tree Functions are Well-Quasi-Ordered | 2022-07-21 | Paper |
Toward neural-network-guided program synthesis and verification
(available as arXiv preprint) | 2022-06-17 | Paper |
Symbolic automatic relations and their applications to SMT and CHC solving
(available as arXiv preprint) | 2022-06-17 | Paper |
scientific article; zbMATH DE number 7471675 (Why is no real title available?)
(available as arXiv preprint) | 2022-02-09 | Paper |
| scientific article; zbMATH DE number 7471675 (Why is no real title available?) | 2022-02-09 | Paper |
Fold/unfold transformations for fixpoint logic
Tools and Algorithms for the Construction and Analysis of Systems | 2021-11-10 | Paper |
| Predicate abstraction and CEGAR for \(\nu \mathrm{HFL}_\mathbb{Z}\) validity checking | 2021-10-18 | Paper |
| A new refinement type system for automated \(\nu\text{HFL}_\mathbb{Z}\) validity checking | 2021-07-08 | Paper |
On the termination problem for probabilistic higher-order recursive programs
(available as arXiv preprint) | 2020-11-03 | Paper |
| On the termination problem for probabilistic higher-order recursive programs | 2020-11-03 | Paper |
ICE-based refinement type discovery for higher-order functional programs
Journal of Automated Reasoning | 2020-11-02 | Paper |
Pumping Lemma for Higher-order Languages
(available as arXiv preprint) | 2020-05-27 | Paper |
| Streett Automata Model Checking of Higher-Order Recursion Schemes | 2020-05-26 | Paper |
ICE-based refinement type discovery for higher-order functional programs
Tools and Algorithms for the Construction and Analysis of Systems | 2019-09-16 | Paper |
Higher-order program verification via HFL model checking
(available as arXiv preprint) | 2019-09-13 | Paper |
Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable
Theoretical Computer Science | 2019-06-18 | Paper |
scientific article; zbMATH DE number 7029315 (Why is no real title available?)
(available as arXiv preprint) | 2019-02-25 | Paper |
| Equivalence-based abstraction refinement for HORS model checking | 2018-10-25 | Paper |
Automata-Based Abstraction Refinement for µHORS Model Checking
2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science | 2018-04-23 | Paper |
| Predicate abstraction and CEGAR for disproving termination of higher-order functional programs | 2018-03-01 | Paper |
On word and frontier languages of unsafe higher-order grammars
(available as arXiv preprint) | 2017-12-19 | Paper |
On the relationship between higher-order recursion schemes and higher-order fixpoint logic
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages | 2017-10-20 | Paper |
Pumping by typing
2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science | 2017-07-03 | Paper |
Modular verification of higher-order functional programs
Programming Languages and Systems | 2017-05-19 | Paper |
Almost every simply typed -term has a long -reduction sequence
Lecture Notes in Computer Science | 2017-05-19 | Paper |
Functional programs as compressed data
Higher-Order and Symbolic Computation | 2017-05-15 | Paper |
Automatically disproving fair termination of higher-order functional programs
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming | 2017-05-10 | Paper |
Compact bit encoding schemes for simply-typed lambda-terms
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming | 2017-05-10 | Paper |
| Saturation-Based Model Checking of Higher-Order Recursion Schemes. | 2017-02-02 | Paper |
Deadlock analysis of unbounded process networks
Information and Computation | 2016-12-22 | Paper |
Higher-order model checking in direct style
Programming Languages and Systems | 2016-12-21 | Paper |
Verification of higher-order concurrent programs with dynamic resource creation
Programming Languages and Systems | 2016-12-21 | Paper |
Temporal verification of higher-order functional programs
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2016-10-24 | Paper |
Verification of tree-processing programs via higher-order model checking
Mathematical Structures in Computer Science | 2016-07-27 | Paper |
A ZDD-Based Efficient Higher-Order Model Checking Algorithm
Programming Languages and Systems | 2016-02-26 | Paper |
Automata-based abstraction for automated verification of higher-order tree-processing programs
Programming Languages and Systems | 2016-01-08 | Paper |
Decision algorithms for checking definability of order-2 finitary PCF
Programming Languages and Systems | 2016-01-08 | Paper |
Types and higher-order recursion schemes for verification of higher-order programs
Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-07-03 | Paper |
Higher-order multi-parameter tree transducers and recursion schemes for program verification
Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-06-11 | Paper |
A generic type system for the -calculus
Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-03-17 | Paper |
Resource usage analysis
Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-03-17 | Paper |
Practical alternating parity tree automata model checking of higher-order recursion schemes
Programming Languages and Systems | 2015-01-12 | Paper |
Automating relatively complete verification of higher-order functional programs
Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2014-11-27 | Paper |
Deadlock analysis of unbounded process networks
CONCUR 2014 – Concurrency Theory | 2014-09-15 | Paper |
Pairwise reachability analysis for higher order concurrent programs by higher-order model checking
CONCUR 2014 – Concurrency Theory | 2014-09-15 | Paper |
Complexity of model-checking call-by-value programs
Lecture Notes in Computer Science | 2014-04-16 | Paper |
Automatic Termination Verification for Higher-Order Functional Programs
Programming Languages and Systems | 2014-04-16 | Paper |
Unsafe order-2 tree languages are context-sensitive
Lecture Notes in Computer Science | 2014-04-16 | Paper |
Model checking higher-order programs
Journal of the ACM | 2014-02-17 | Paper |
A Coq library for verification of concurrent programs
Electronic Notes in Theoretical Computer Science | 2014-01-10 | Paper |
| Partial order reduction for verification of spatial properties of pi-calculus processes | 2013-09-25 | Paper |
Model-checking higher-order programs with recursive types
Programming Languages and Systems | 2013-08-05 | Paper |
An intersection type system for deterministic pushdown automata
Lecture Notes in Computer Science | 2012-09-21 | Paper |
Exact flow analysis by higher-order model checking
Functional and Logic Programming | 2012-07-20 | Paper |
Type-based automated verification of authenticity in asymmetric cryptographic protocols
Automated Technology for Verification and Analysis | 2011-10-07 | Paper |
A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes
Foundations of Software Science and Computational Structures | 2011-05-19 | Paper |
Untyped Recursion Schemes and Infinite Intersection Types
Foundations of Software Science and Computational Structures | 2010-04-27 | Paper |
Type systems for concurrent programs.
Lecture Notes in Computer Science | 2010-03-30 | Paper |
Higher-order program verification and language-based security (extended abstract)
Advances in Computer Science - ASIAN 2009. Information Security and Privacy | 2010-01-14 | Paper |
Useless-code elimination and program slicing for the pi-calculus.
Lecture Notes in Computer Science | 2010-01-05 | Paper |
Undecidable equivalences for basic parallel processes
Information and Computation | 2009-07-15 | Paper |
Type-Based Automated Verification of Authenticity in Cryptographic Protocols
Programming Languages and Systems | 2009-03-31 | Paper |
Extension of Type-Based Approach to Generation of Stream-Processing Programs by Automatic Insertion of Buffering Primitives
Logic Based Program Synthesis and Transformation | 2009-01-15 | Paper |
A new type system for JVM lock primitives
New Generation Computing | 2008-10-20 | Paper |
Tree Automata for Non-linear Arithmetic
Rewriting Techniques and Applications | 2008-08-28 | Paper |
| Maximum distributions of bridges of noncolliding Brownian paths | 2008-08-27 | Paper |
Two Bessel bridges conditioned never to collide, double Dirichlet series, and Jacobi theta function
Journal of Statistical Physics | 2008-08-20 | Paper |
A Hybrid Type System for Lock-Freedom of Mobile Processes
Computer Aided Verification | 2008-07-15 | Paper |
Logical Bisimulations and Functional Languages
Lecture Notes in Computer Science | 2008-07-01 | Paper |
Translation of tree-processing programs into stream-processing programs based on ordered linear type
Journal of Functional Programming | 2008-05-22 | Paper |
Type-Based Verification of Correspondence Assertions for Communication Protocols
Programming Languages and Systems | 2008-05-15 | Paper |
Substructural Type Systems for Program Analysis
Functional and Logic Programming | 2008-04-11 | Paper |
On-Demand Refinement of Dependent Types
Functional and Logic Programming | 2008-04-11 | Paper |
Linear Declassification
Programming Languages and Systems | 2008-04-11 | Paper |
| Limit distributions of two-dimensional quantum walks | 2008-02-19 | Paper |
Undecidability of 2-Label BPP Equivalences and Behavioral Type Systems for the π-Calculus
Automata, Languages and Programming | 2007-11-28 | Paper |
Resource Usage Analysis for the Pi-Calculus
Logical Methods in Computer Science | 2007-10-11 | Paper |
A New Type System for Deadlock-Free Processes
CONCUR 2006 – Concurrency Theory | 2007-09-04 | Paper |
Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts
Programming Languages and Systems | 2007-09-04 | Paper |
Verification, Model Checking, and Abstract Interpretation
Lecture Notes in Computer Science | 2007-02-12 | Paper |
A type system for lock-free processes
Information and Computation | 2006-08-03 | Paper |
Type-based information flow analysis for the \(\pi\)-calculus
Acta Informatica | 2006-01-10 | Paper |
Programming Languages and Systems
Lecture Notes in Computer Science | 2005-08-17 | Paper |
Programming Languages and Systems
Lecture Notes in Computer Science | 2005-08-17 | Paper |
Dynamic Scaling of the Growing Rough Surfaces
Journal of the Physical Society of Japan | 2005-03-21 | Paper |
A generic type system for the pi-calculus
Theoretical Computer Science | 2004-10-27 | Paper |
| scientific article; zbMATH DE number 1962749 (Why is no real title available?) | 2003-08-11 | Paper |
| scientific article; zbMATH DE number 1962750 (Why is no real title available?) | 2003-08-11 | Paper |
Type reconstruction for linear \(\pi\)-calculus with I/O subtyping.
Information and Computation | 2003-01-14 | Paper |
| scientific article; zbMATH DE number 1759483 (Why is no real title available?) | 2002-11-25 | Paper |
| scientific article; zbMATH DE number 1759631 (Why is no real title available?) | 2002-06-25 | Paper |
A hybrid approach to online and offline partial evaluation
Higher-Order and Symbolic Computation | 2002-03-14 | Paper |
Type-based useless-variable elimination
Higher-Order and Symbolic Computation | 2002-03-14 | Paper |
Distributed concurrent linear logic programming
Theoretical Computer Science | 2000-08-23 | Paper |
| scientific article; zbMATH DE number 1404223 (Why is no real title available?) | 2000-02-20 | Paper |
| scientific article; zbMATH DE number 1304382 (Why is no real title available?) | 1999-06-17 | Paper |
| scientific article; zbMATH DE number 1231692 (Why is no real title available?) | 1999-01-10 | Paper |
Asynchronous communication model based on linear logic
Formal Aspects of Computing | 1995-09-25 | Paper |
