Mauricio Ayala-Rincón

Sci. Comput. Program., 2020

Introduction to the special issue: Unification.

[BibT_eX]

[DOI]

Philippe Balbiani

Math. Struct. Comput. Sci., 2020

On Nominal Syntax and Permutation Fixed Points.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2020

Teaching Interactive Proofs to Mathematicians.

[BibT_eX]

[DOI]

Thaynara Arielly de Lima

CoRR, 2020

On Solving Nominal Disunification Constraints.

[BibT_eX]

[DOI]

Deivid Val

Proceedings of the 14th Workshop on Logical and Semantic Frameworks with Applications, 2020

Behavior of Bioinspired Algorithms in Parallel Island Models.

[BibT_eX]

[DOI]

Proceedings of the IEEE Congress on Evolutionary Computation, 2020

2019

A formalisation of nominal α-equivalence with A, C, and AC function symbols.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2019

Typed path polymorphism.

[BibT_eX]

[DOI]

Eduardo Bonelli

Juan Edi

Andrés Viso

Theor. Comput. Sci., 2019

Selected Extended Papers of ITP 2017 - Preface.

[BibT_eX]

[DOI]

J. Autom. Reason., 2019

Opposition-Based Memetic Algorithm and Hybrid Approach for Sorting Permutations by Reversals.

[BibT_eX]

[DOI]

Evol. Comput., 2019

The Computational Relevance of Formal Logic Through Formal Proofs.

[BibT_eX]

[DOI]

Ariane Alves Almeida

Thiago Mendonça Ferreira Ramos

Proceedings of the Formal Methods Teaching - Third International Workshop and Tutorial, 2019

Application of an Adaptive Genetic Algorithm for Task Mapping Optimisation on a Wormhole-based Real-time Network-on-Chip.

[BibT_eX]

[DOI]

Jessé Barreto de Barros

Carlos Humberto Llanos Quintero

Proceedings of the IX Brazilian Symposium on Computing Systems Engineering, 2019

A Certified Functional Nominal C-Unification Algorithm.

[BibT_eX]

[DOI]

Gabriel Ferreira Silva

Proceedings of the Logic-Based Program Synthesis and Transformation, 2019

Parallel Island Model Genetic Algorithms applied in NP-Hard problems.

[BibT_eX]

[DOI]

Proceedings of the IEEE Congress on Evolutionary Computation, 2019

2018

Nominal essential intersection types.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2018

A Formalisation of Nominal C-Matching through Unification with Protected Variables.

[BibT_eX]

[DOI]

Proceedings of the 13th Workshop on Logical and Semantic Frameworks with Applications, 2018

On the average number of reversals needed to sort signed permutations.

[BibT_eX]

[DOI]

Thiago Mendonça Ferreira Ramos

Discret. Appl. Math., 2018

Formalization of the Undecidability of the Halting Problem for a Functional Language.

[BibT_eX]

[DOI]

Mariano M. Moscato

Aaron Dutle

Anthony Narkawicz

Proceedings of the Logic, Language, Information, and Computation, 2018

Fixed-Point Constraints for Nominal Equational Unification.

[BibT_eX]

[DOI]

Daniel Saad Nogueira Nunes

Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, 2018

A Grammar Compression Algorithm Based on Induced Suffix Sorting.

[BibT_eX]

[DOI]

Felipe A. Louza

Simon Gog

Gonzalo Navarro

Proceedings of the 2018 Data Compression Conference, 2018

Parallel Multi-Island Genetic Algotirth for Sorting Unsigned Genomes by Reversals.

[BibT_eX]

[DOI]

Proceedings of the 2018 IEEE Congress on Evolutionary Computation, 2018

2017

Applied Logic for Computer Scientists - Computational Deduction and Formal Proofs

[BibT_eX]

[DOI]

Undergraduate Topics in Computer Science, Springer, ISBN: 978-3-319-51653-0, 2017

Logical and Semantic Frameworks with Applications.

[BibT_eX]

[DOI]

Ian Mackie

Ugo Montanari

Theor. Comput. Sci., 2017

Intruder deduction problem for locally stable theories with normal forms and inverses.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 2017

Confluence of Orthogonal Term Rewriting Systems in the Prototype Verification System.

[BibT_eX]

[DOI]

J. Autom. Reason., 2017

Nominal C-Unification.

[BibT_eX]

[DOI]

Proceedings of the Logic-Based Program Synthesis and Transformation, 2017

On Solving Nominal Fixpoint Equations.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

Variable neighborhood search for the large phylogeny problem using gene order data.

[BibT_eX]

[DOI]

Proceedings of the 2017 IEEE Congress on Evolutionary Computation, 2017

Parallel genetic algorithms with sharing of individuals for sorting unsigned genomes by reversals.

[BibT_eX]

[DOI]

Lucas Angelo da Silveira

Daniel Saad Nogueira Nunes

Proceedings of the 2017 IEEE Congress on Evolutionary Computation, 2017

2016

A Practical Semi-External Memory Method for Approximate Pattern Matching.

[BibT_eX]

[DOI]

Electron. Notes Theor. Comput. Sci., 2016

A Formalisation of Nominal α-equivalence with A and AC Function Symbols.

[BibT_eX]

[DOI]

Proceedings of the 11th Workshop on Logical and Semantic Frameworks with Applications, 2016

Nominal Narrowing.

[BibT_eX]

[DOI]

Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction, 2016

Parallel memetic genetic algorithms for sorting unsigned genomes by translocations.

[BibT_eX]

[DOI]

Proceedings of the IEEE Congress on Evolutionary Computation, 2016

2015

Parallelization of genetic algorithms for sorting permutations by reversals over biological data.

[BibT_eX]

[DOI]

Gabriel Marchesan Almeida

Jürgen Becker

Int. J. Hybrid Intell. Syst., 2015

Explicit substitution calculi with de Bruijn indices and intersection type systems.

[BibT_eX]

[DOI]

Log. J. IGPL, 2015

Type Soundness for Path Polymorphism.

[BibT_eX]

[DOI]

Andrés Viso

Eduardo Bonelli

Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications, 2015

Completeness in PVS of a Nominal Unification Algorithm.

[BibT_eX]

[DOI]

Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications, 2015

Checking Overlaps of Nominal Rewriting Rules.

[BibT_eX]

[DOI]

Murdoch James Gabbay

Proceedings of the Tenth Workshop on Logical and Semantic Frameworks, with Applications, 2015

Formalising Confluence in PVS.

[BibT_eX]

[DOI]

Proceedings of the Eleventh International Workshop on Developments in Computational Models, 2015

Memetic and Opposition-Based Learning Genetic Algorithms for Sorting Unsigned Genomes by Translocations.

[BibT_eX]

[DOI]

Proceedings of the Advances in Nature and Biologically Inspired Computing, 2015

Computing translocation distance by a genetic algorithm.

[BibT_eX]

[DOI]

Proceedings of the 2015 Latin American Computing Conference, 2015

2014

First-order unification in the PVS proof assistant.

[BibT_eX]

[DOI]

Andréia Borges Avelar

Flávio Leonardo Cavalcanti de Moura

Log. J. IGPL, 2014

Preface.

[BibT_eX]

[DOI]

Ian Mackie

Proceedings of the Ninth Workshop on Logical and Semantic Frameworks, with Applications, 2014

Hardware opposition-based PSO applied to mobile robot controllers.

[BibT_eX]

[DOI]

Eng. Appl. Artif. Intell., 2014

Verification of Hardware Implementations through Correctness of their Recursive Definitions in PVS.

[BibT_eX]

[DOI]

Ariane Alves Almeida

Janier Arias-Garcia

Proceedings of the 27th Symposium on Integrated Circuits and Systems Design, 2014

On the Computability of Relations on λ-Terms and Rice's Theorem - The Case of the Expansion Problem for Explicit Substitutions.

[BibT_eX]

[DOI]

Edward Hermann Haeusler

Proceedings of the LATIN 2014: Theoretical Informatics - 11th Latin American Symposium, Montevideo, Uruguay, March 31, 2014

Metaconfluence of Calculi with Explicit Substitutions at a Distance.

[BibT_eX]

[DOI]

Delia Kesner

Proceedings of the 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, 2014

Memetic algorithm for sorting unsigned permutations by reversals.

[BibT_eX]

[DOI]

Proceedings of the IEEE Congress on Evolutionary Computation, 2014

2013

Formalization in PVS of Balancing Properties Necessary for Proving Security of the Dolev-Yao Cascade Protocol Model.

[BibT_eX]

[DOI]

Daniel Saad Nogueira Nunes

Yuri Santos Rego

J. Formaliz. Reason., 2013

A Compressed Suffix Tree Based Implementation With Low Peak Memory Usage.

[BibT_eX]

[DOI]

Proceedings of the XXXIX Latin American Computer Conference - Selected Papers, 2013

Parallelization and virtualization of genetic algorithms for sorting permutations by reversals.

[BibT_eX]

[DOI]

Gabriel Marchesan Almeida

Jürgen Becker

Proceedings of the Fifth World Congress on Nature and Biologically Inspired Computing, 2013

Hardware-based parallel firefly algorithm for embedded applications.

[BibT_eX]

[DOI]

Proceedings of the 2013 NASA/ESA Conference on Adaptive Hardware and Systems, 2013

2012

Sorting Permutations by Reversals through a Hybrid Genetic Algorithm based on Breakpoint Elimination and Exact Solutions for Signed Permutations.

[BibT_eX]

[DOI]

Proceedings of the XXXVIII Latin American Computer Conference - Selected Papers, 2012

Formalizing the Confluence of Orthogonal Rewriting Systems

[BibT_eX]

[DOI]

Proceedings of the Proceedings Seventh Workshop on Logical and Semantic Frameworks, 2012

Elementary Deduction Problem for Locally Stable Theories with Normal Forms

[BibT_eX]

[DOI]

Daniele Nantes Sobrinho

Proceedings of the Proceedings Seventh Workshop on Logical and Semantic Frameworks, 2012

2011

Preface.

[BibT_eX]

[DOI]

Elaine Pimentel

Theor. Comput. Sci., 2011

A Formalization of the Theorem of Existence of First-Order Most General Unifiers

[BibT_eX]

[DOI]

Andréia B. Avelar

Proceedings of the Proceedings 6th Workshop on Logical and Semantic Frameworks with Applications, 2011

Opposition-based shuffled PSO with passive congregation applied to FM matching synthesis.

[BibT_eX]

[DOI]

Proceedings of the IEEE Congress on Evolutionary Computation, 2011

2010

A Formalization of the Knuth-Bendix(-Huet) Critical Pair Theorem.

[BibT_eX]

[DOI]

J. Autom. Reason., 2010

A Flexible Framework for Visualisation of Computational Properties of General Explicit Substitutions Calculi.

[BibT_eX]

[DOI]

A. V. Barbosa

Proceedings of the Fifth Logical and Semantic Frameworks, with Applications Workshop, 2010

Intersection Type Systems and Explicit Substitutions Calculi.

[BibT_eX]

[DOI]

Proceedings of the Logic, 2010

Reduction of the Intruder Deduction Problem into Equational Elementary Deduction for Electronic Purse Protocols with Blind Signatures.

[BibT_eX]

[DOI]

Daniele Nantes Sobrinho

Proceedings of the Logic, 2010

Verification of the Completeness of Unification Algorithms à la Robinson.

[BibT_eX]

[DOI]

Andréia B. Avelar

Proceedings of the Logic, 2010

Hardware Particle Swarm Optimization Based on the Attractive-Repulsive Scheme for Embedded Applications.

[BibT_eX]

[DOI]

Proceedings of the ReConFig'10: 2010 International Conference on Reconfigurable Computing and FPGAs, 2010

Comparison between two FPGA implementations of the Particle Swarm Optimization algorithm for high-performance embedded applications.

[BibT_eX]

[DOI]

Proceedings of the Fifth International Conference on Bio-Inspired Computing: Theories and Applications, 2010

Accelerating the Shuffled Frog Leaping algorithm by parallel implementations in FPGAs.

[BibT_eX]

[DOI]

Proceedings of the Fifth International Conference on Bio-Inspired Computing: Theories and Applications, 2010

2009

Explicit substitutions calculi with one step Eta-reduction decided explicitly.

[BibT_eX]

[DOI]

Log. J. IGPL, 2009

Preface.

[BibT_eX]

[DOI]

Proceedings of the Fourth Workshop on Logical and Semantic Frameworks, with Applications, 2009

Principal Typings in a Restricted Intersection Type System for Beta Normal Forms with De Bruijn Indices

[BibT_eX]

[DOI]

Proceedings of the Proceedings Ninth International Workshop on Reduction Strategies in Rewriting and Programming, 2009

Parameterizable floating-point library for arithmetic operations in FPGAs.

[BibT_eX]

[DOI]

Diego F. Sánchez

Proceedings of the 22st Annual Symposium on Integrated Circuits and Systems Design: Chip on the Dunes, 2009

Hardware Architecture for Particle Swarm Optimization Using Floating-Point Arithmetic.

[BibT_eX]

[DOI]

Daniel M. Muñoz Arboleda

Proceedings of the Ninth International Conference on Intelligent Systems Design and Applications, 2009

2008

A Formalization of Newman's and Yokouchi's Lemmas in a Higher-Order Language.

[BibT_eX]

[DOI]

J. Formaliz. Reason., 2008

Higher-Order Unification: A structural relation between Huet's method and the one based on explicit substitutions.

[BibT_eX]

[DOI]

J. Appl. Log., 2008

A PVS Theory for Term Rewriting Systems.

[BibT_eX]

[DOI]

Proceedings of the Third Workshop on Logical and Semantic Frameworks with Applications, 2008

Distributed approach to group control of elevator systems using fuzzy logic and FPGA implementation of dispatching algorithms.

[BibT_eX]

[DOI]

Rudi H. van Els

Eng. Appl. Artif. Intell., 2008

A Theory for Abstract Reduction Systems in PVS.

[BibT_eX]

[DOI]

CLEI Electron. J., 2008

Principal Typings for Explicit Substitutions Calculi.

[BibT_eX]

[DOI]

Proceedings of the Logic and Theory of Algorithms, 2008

2007

Parallel strategies for the local biological sequence alignment in a cluster of workstations.

[BibT_eX]

[DOI]

Maria Emilia Telles Walter

J. Parallel Distributed Comput., 2007

A variant of the Ford-Johnson algorithm that is more space efficient.

[BibT_eX]

Bruno T. de Abreu

José de Siqueira

Inf. Process. Lett., 2007

Preface.

[BibT_eX]

[DOI]

Edward Hermann Haeusler

Proceedings of the Second Workshop on Logical and Semantic Frameworks, with Applications, 2007

An exact parallel algorithm to compare very long biological sequences in clusters of workstations.

[BibT_eX]

[DOI]

Edans Flavius de Oliveira Sandes

Clust. Comput., 2007

Formal Verification of an Optimal Air Traffic Conflict Resolution and Recovery Algorithm.

[BibT_eX]

[DOI]

Proceedings of the Logic, 2007

2006

Prototyping time- and space-efficient computations of algebraic operations over dynamically reconfigurable systems modeled by rewriting-logic.

[BibT_eX]

[DOI]

ACM Trans. Design Autom. Electr. Syst., 2006

SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi.

[BibT_eX]

[DOI]

J. Appl. Non Class. Logics, 2006

Implementation of dispatching algorithms for elevator systems using reconfigurable architectures.

[BibT_eX]

[DOI]

Rudi H. van Els

Renato P. Almeida

Proceedings of the 19th Annual Symposium on Integrated Circuits and Systems Design, 2006

SAEPTUM: verification of ELAN hardware specifications using the proof assistant PVS.

[BibT_eX]

[DOI]

Thomas Mailleux Santana

Proceedings of the 19th Annual Symposium on Integrated Circuits and Systems Design, 2006

Implementation, Simulation and Validation of Dispatching Algorithms for Elevator Systems.

[BibT_eX]

[DOI]

Rudi H. van Els

Proceedings of the 2006 IEEE International Conference on Reconfigurable Computing and FPGA's, 2006

2005

Comparing and implementing calculi of explicit substitutions with eta-reduction.

[BibT_eX]

[DOI]

Rodrigo de Castro Miranda

Ann. Pure Appl. Log., 2005

A Modification of the Landau-Vishkin Algorithm Computing Longest Common Extensions via Suffix Arrays.

[BibT_eX]

[DOI]

Proceedings of the Advances in Bioinformatics and Computational Biology, 2005

Parallel Smith-Waterman Algorithm for Local DNA Comparison in a Cluster of Workstations.

[BibT_eX]

[DOI]

Thomas Mailleux Santana

Proceedings of the Experimental and Efficient Algorithms, 4th InternationalWorkshop, 2005

VANNGen: a flexible CAD tool for hardware implementation of artificial neural networks.

[BibT_eX]

[DOI]

André L. S. Braga

Proceedings of the 2005 International Conference on Reconfigurable Computing and FPGAs, 2005

Parallel Strategies for Local Biological Sequence Alignment in a Cluster of Workstations.

[BibT_eX]

[DOI]

Thomas Mailleux Santana

Proceedings of the 19th International Parallel and Distributed Processing Symposium (IPDPS 2005), 2005

FELIX: Using Rewriting-Logic for Generating Functionally Equivalent Implementations.

[BibT_eX]

[DOI]

Carlos Morra

Jürgen Becker

Proceedings of the 2005 International Conference on Field Programmable Logic and Applications (FPL), 2005

2004

Reconfigurable Systems for Sequence Alignment and for General Dynamic Programming.

[BibT_eX]

Luis G. A. Carvalho

Proceedings of the III Brazilian Workshop on Bioinformatics, 2004

Modeling and prototyping dynamically reconfigurable systems for efficient computation of dynamic programming methods by rewriting-logic.

[BibT_eX]

[DOI]

Luis G. A. Carvalho

Proceedings of the 17th Annual Symposium on Integrated Circuits and Systems Design, 2004

Second-Order Matching via Explicit Substitutions.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2004

2003

On Automating the Extraction of Programs from Termination Proofs.

[BibT_eX]

[DOI]

François Monin

Rev. Colomb. de Computación, 2003

A Linear Time Lower Bound on McCreight and General Updating Algorithms for Suffix Trees.

[BibT_eX]

[DOI]

Paulo D. Conejo

Algorithmica, 2003

Efficient Computation of Algebraic Operations over Dynamically Reconfigurable Systems Specified by Rewriting-Logic Environments.

[BibT_eX]

[DOI]

Rodrigo B. Nogueira

Proceedings of the 23rd International Conference of the Chilean Computer Science Society (SCCC 2003), 2003

Modeling a Reconfigurable System for Computing the FFT in Place via Rewriting-Logic.

[BibT_eX]

[DOI]

Rodrigo B. Nogueira

Proceedings of the 16th Annual Symposium on Integrated Circuits and Systems Design, 2003

Using Rewriting-Logic Notation for Funcional Verification in Data-Stream Based Reconfigurable Computing.

[BibT_eX]

[DOI]

Proceedings of the Forum on specification and Design Languages, 2003

2002

Architectural Specification, Exploration and Simulation Through Rewriting-Logic.

[BibT_eX]

[DOI]

Rinaldi Maya Neto

Rev. Colomb. de Computación, 2002

A framework to visualize equivalences between computational models of regular languages.

[BibT_eX]

[DOI]

Alexsandro F. da Fonseca

Haydée Werneck Poubel

José de Siqueira

Inf. Process. Lett., 2002

On automating the extraction of programs from proofs using product types.

[BibT_eX]

[DOI]

François Monin

Electron. Notes Theor. Comput. Sci., 2002

Applying ELAN Strategies in Simulating Processors over Simple Architectures.

[BibT_eX]

[DOI]

Rinaldi Maya Neto

Electron. Notes Theor. Comput. Sci., 2002

Comparing Calculi of Explicit Substitutions with Eta-reduction.

[BibT_eX]

[DOI]

Electron. Notes Theor. Comput. Sci., 2002

2001

Unification Modulo Presburger Arithmetic and Other Decidable Theories.

[BibT_eX]

[DOI]

Ivan E. Tavares de Araújo

Rev. Colomb. de Computación, 2001

Unification via the lambda se-Style of Explicit Substitutions.

[BibT_eX]

[DOI]

Log. J. IGPL, 2001

An Efficient Strategy for Word-Cycle Completion in Finitely Presented Groups.

[BibT_eX]

[DOI]

Luiz M. R. Gadelha Jr.

Proceedings of the 21st International Conference of the Chilean Computer Science Society (SCCC 2001), 2001

2000

Explicit Substitions and All That.

[BibT_eX]

[DOI]

Rev. Colomb. de Computación, 2000

Unification via se-style of explicit substitution.

[BibT_eX]

[DOI]

Proceedings of the 2nd international ACM SIGPLAN conference on on Principles and practice of declarative programming, 2000

1998

A Linear Time Lower Bound on Updating Algorithms for Suffix Trees.

[BibT_eX]

[DOI]

Paulo D. Conejo

Proceedings of the String Processing and Information Retrieval: A South American Symposium, 1998

1993

Expressiveness of conditional equational systems with built-in predicates.

[BibT_eX]

[DOI]