| Publication | Date of Publication | Type |
|---|
| A PVS library on the infinitude of primes | 2026-02-19 | Paper |
| Graded quantitative narrowing | 2026-02-19 | Paper |
| A formalization of the general theory of quaternions | 2026-02-10 | Paper |
A nominal approach to equational problems in languages with binders
ACM Transactions on Computational Logic | 2026-01-07 | Paper |
| Nominal equational rewriting and narrowing | 2025-09-03 | Paper |
| Formalizing factorization on Euclidean domains and abstract Euclidean algorithms | 2025-09-03 | Paper |
| Formalization of algebraic theorems in PVS (invited talk) | 2025-02-19 | Paper |
Certified first-order AC-unification and applications.
Journal of Automated Reasoning | 2025-02-07 | Paper |
| Equational anti-unification over absorption theories | 2025-01-31 | Paper |
| A certified algorithm for AC-unification | 2024-05-27 | Paper |
Grammar Compression by Induced Suffix Sorting
ACM Journal of Experimental Algorithmics | 2024-04-14 | Paper |
Nominal AC-matching
Lecture Notes in Computer Science | 2024-02-28 | Paper |
Formal verification of termination criteria for first-order recursive functions
Journal of Automated Reasoning | 2024-02-06 | Paper |
| scientific article; zbMATH DE number 7699444 (Why is no real title available?) | 2023-06-20 | Paper |
Hall's theorem for enumerable families of finite sets
Lecture Notes in Computer Science | 2023-06-02 | Paper |
Formalization of the computational theory of a Turing complete functional language model
Journal of Automated Reasoning | 2022-12-12 | Paper |
A certified functional nominal C-unification algorithm
Logic-Based Program Synthesis and Transformation | 2022-08-25 | Paper |
Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem
Journal of Automated Reasoning | 2022-01-21 | Paper |
Formalising nominal C-unification generalised with protected variables
Mathematical Structures in Computer Science | 2022-01-20 | Paper |
Formalising confluence in PVS
(available as arXiv preprint) | 2021-12-02 | Paper |
| Formalising confluence in PVS | 2021-12-02 | Paper |
| Nominal equational problems | 2021-10-18 | Paper |
| Fixed-point constraints for nominal equational unification | 2021-06-15 | Paper |
Elementary deduction problem for locally stable theories with normal forms
(available as arXiv preprint) | 2021-06-08 | Paper |
| Elementary deduction problem for locally stable theories with normal forms | 2021-06-08 | Paper |
Formalizing the confluence of orthogonal rewriting systems
(available as arXiv preprint) | 2021-06-08 | Paper |
| Formalizing the confluence of orthogonal rewriting systems | 2021-06-08 | Paper |
| On solving nominal disunification constraints | 2021-01-19 | Paper |
On nominal syntax and permutation fixed points
(available as arXiv preprint) | 2020-02-17 | Paper |
| A formalisation of nominal C-matching through unification with protected variables | 2019-11-13 | Paper |
| Formalization in PVS of balancing properties necessary for proving security of the Dolev-Yao cascade protocol model | 2019-09-18 | Paper |
A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols
Theoretical Computer Science | 2019-06-25 | Paper |
Typed path polymorphism
Theoretical Computer Science | 2019-06-25 | Paper |
Explicit substitution calculi with de Bruijn indices and intersection type systems
Logic Journal of the IGPL | 2019-01-08 | Paper |
First-order unification in the PVS proof assistant
Logic Journal of the IGPL | 2019-01-08 | Paper |
Applied logic for computer scientists. Computational deduction and formal proofs
Undergraduate Topics in Computer Science | 2018-11-29 | Paper |
| Formalization of the undecidability of the halting problem for a functional language | 2018-10-18 | Paper |
Nominal C-unification
(available as arXiv preprint) | 2018-09-06 | Paper |
Nominal essential intersection types
Theoretical Computer Science | 2018-06-18 | Paper |
| Checking overlaps of nominal rewriting rules | 2018-04-23 | Paper |
| Completeness in PVS of a nominal unification algorithm | 2018-04-23 | Paper |
Type soundness for path polymorphism
(available as arXiv preprint) | 2018-04-23 | Paper |
| A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols | 2018-04-23 | Paper |
Intruder deduction problem for locally stable theories with normal forms and inverses
Theoretical Computer Science | 2018-02-09 | Paper |
| On solving nominal fixpoint equations | 2018-01-04 | Paper |
On the average number of reversals needed to sort signed permutations
Discrete Applied Mathematics | 2017-12-06 | Paper |
| Nominal narrowing | 2017-10-17 | Paper |
Confluence of orthogonal term rewriting systems in the prototype verification system
Journal of Automated Reasoning | 2017-07-06 | Paper |
| A practical semi-external memory method for approximate pattern matching | 2017-05-19 | Paper |
| scientific article; zbMATH DE number 6707782 (Why is no real title available?) | 2017-04-25 | Paper |
A PVS theory for term rewriting systems
Electronic Notes in Theoretical Computer Science | 2015-03-18 | Paper |
A flexible framework for visualisation of computational properties of general explicit substitutions calculi
Electronic Notes in Theoretical Computer Science | 2015-03-18 | Paper |
On the computability of relations on \(\lambda \)-terms and Rice's theorem -- the case of the expansion problem for explicit substitutions
LATIN 2014: Theoretical Informatics | 2014-03-31 | Paper |
| Applying ELAN strategies in simulating processors over simple architectures | 2013-08-23 | Paper |
Comparing calculi of explicit substitutions with eta-reduction
Electronic Notes in Theoretical Computer Science | 2013-04-19 | Paper |
On automating the extraction of programs from proofs using product types
Electronic Notes in Theoretical Computer Science | 2013-04-19 | Paper |
| Intersection type system with de Bruijn indices | 2011-03-30 | Paper |
Verification of the Completeness of Unification Algorithms à la Robinson
Logic, Language, Information and Computation | 2010-09-29 | Paper |
Reduction of the intruder deduction problem into equational elementary deduction for electronic purse protocols with blind signatures
Logic, Language, Information and Computation | 2010-09-29 | Paper |
Intersection type systems and explicit substitutions calculi
Logic, Language, Information and Computation | 2010-09-29 | Paper |
A variant of the Ford-Johnson algorithm that is more space efficient
Information Processing Letters | 2010-01-29 | Paper |
Explicit substitutions calculi with one step eta-reduction decided explicitly
Logic Journal of the IGPL | 2009-12-18 | Paper |
SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi
Journal of Applied Non-Classical Logics | 2009-11-30 | Paper |
| A formalization of Newman's and Yokouchi's lemmas in a higher-order language | 2009-07-27 | Paper |
Principal Typings for Explicit Substitutions Calculi
Logic and Theory of Algorithms | 2008-06-19 | Paper |
Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions
Journal of Applied Logic | 2008-04-07 | Paper |
Parallel strategies for the local biological sequence alignment in a cluster of workstations
Journal of Parallel and Distributed Computing | 2007-02-14 | Paper |
Experimental and Efficient Algorithms
Lecture Notes in Computer Science | 2005-11-30 | Paper |
Logic for Programming, Artificial Intelligence, and Reasoning
Lecture Notes in Computer Science | 2005-11-10 | Paper |
| scientific article; zbMATH DE number 2208065 (Why is no real title available?) | 2005-09-26 | Paper |
Comparing and implementing calculi of explicit substitutions with eta-reduction
Annals of Pure and Applied Logic | 2005-06-01 | Paper |
A linear time lower bound on McCreight and general updating algorithms for suffix trees
Algorithmica | 2004-09-22 | Paper |
A framework to visualize equivalences between computational models of regular languages.
Information Processing Letters | 2003-01-21 | Paper |
Unification via the s_e-style of explicit substitutions
Logic Journal of the IGPL | 2002-06-19 | Paper |
| Church-Rosser property for conditional rewriting systems with built-in predicates as premises | 2002-04-03 | Paper |
| scientific article; zbMATH DE number 1274721 (Why is no real title available?) | 1999-04-13 | Paper |
