| Publication | Date of Publication | Type |
|---|
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
| 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
| 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
| 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
| 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
| 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 |
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 |
Verification of the Completeness of Unification Algorithms à la Robinson
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 \(\lambda 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 |
