Proceedings of the ACM on Programming Languages, 6(OOPSLA2), 758-785

A miniKanren é uma linguagem embutida leve para programação lógica e relacional. Muitas das suas características úteis vêm de uma estratégia de busca peculiar chamada busca por intercalação. Porém, a busca por intercalação torna irrelevantes as formas convencionais de raciocínio sobre a complexidade e o desempenho de programas lógicos. Identificamos um importante componente-chave — o agendamento — que torna o raciocínio tão diferente na miniKanren e apresentamos uma técnica semiautomática para estimar o impacto do agendamento através da execução simbólica de uma classe razoavelmente ampla de programas.

49º Simpósio ACM SIGPLAN sobre Princípios de Linguagens de Programação (POPL 2012)

Scientific and Technical Journal of Information Technologies, Mechanics and Optics

Syrcose'21

TFPIE-2021

Prêmio de Artigo de Destaque no OOPSLA'21

OOPSLA

Programming and Computer Software Journal

Apresentamos uma nova estratégia equilibrada de avaliação de execuções conjuntas para a linguagem de programação relacional miniKanren. Ao contrário das execuções conjuntas originais com viés à esquerda, nossa abordagem controla a ordem da execução conjunta com base nas propriedades intrínsecas das definições das relações. Apresentamos tanto um estudo formal do equilíbrio das execuções conjuntas quanto uma avaliação prática que demonstra as melhorias essenciais, tanto em termos de desempenho quanto de convergência.

SEIM-2021

ICPP-2021

Apresentamos um estudo formal da semântica da linguagem de programação relacional miniKanren. Primeiro, formulamos uma semântica denotativa que corresponde ao modelo mínimo de Herbrand para programas de lógica definida. Depois, apresentamos uma semântica operacional que modela a intercalação, que é a característica distintiva da implementação da miniKanren, e provamos sua validade e completude no que diz respeito à semântica denotativa. Nosso desenvolvimento tem o apoio de uma especificação de Coq, da qual se pode extrair um interpretador de referência. Também derivamos do nosso resultado principal uma semântica certificada (e um interpretador de referência) para resolução SLD com corte e provamos sua validade.

Apresentamos uma abordagem totalmente declarativa da síntese de implementações de construtos de correspondência de padrões, baseada na aplicação da programação relacional, uma forma específica de programação com lógica por restrições. Nossa abordagem é baseada em representações relacionais tanto da semântica de alto nível da correspondência de padrões quanto da semântica de uma linguagem de implementação de nível intermediário. Essa escolha torna a nossa abordagem, em princípio, bastante escalável, pois precisamos apenas modificar a semântica de alto nível para sintetizar a implementação de um novo recurso de correspondência de padrões. Nossa avaliação de um conjunto de amostras pequenas, parcialmente extraídas da literatura, mostra que nosso framework é capaz de rapidamente sintetizar implementações otimizadas. Porém, nossa avaliação profunda de estresse em diversos testes artificiais de desempenho mostrou a necessidade de futuras melhorias.

Consultas de caminhos sem contexto (CFPQ) ampliam o alcance das consultas normais de caminhos (RPQ), por permitirem que gramáticas sem contexto sejam utilizadas como restrições de caminhos. Algoritmos de CFPQ estão sendo desenvolvidos ativamente, mas J. Kuijpers at al. concluíram recentemente que os algoritmos existentes não têm desempenho suficiente para serem utilizados em aplicações no mundo real. Assim, justifica-se o desenvolvimento de novos algoritmos de CFPQ. Neste artigo, apresentamos um novo algoritmo de CFPQ, baseado em operações de álgebra linear, tais como o produto de Kronecker e o fechamento transitivo, que trata as gramáticas apresentadas como máquinas de estado recursivas. Assim, o algoritmo proposto pode ser implementado através de bibliotecas de alto desempenho e de hardware paralelo moderno. Além disso, o algoritmo evita o crescimento das gramáticas e isso traz a possibilidade da otimização de consultas.

ADBIS 2020. Advances in Databases and Information Systems. Anotações de Palestras de Ciências da Computação.

São usadas expressões regulares em caminhos de propriedades em SPARQL para consultar grafos em RDF. Porém, expressões regulares só podem definir a classe mais limitada de linguagens, chamadas de linguagens regulares. Linguagens sem contexto são uma classe mais ampla que contém todas as linguagens regulares. Não existem expressões sem contexto para defini-las, de modo que é necessário escrever gramáticas. Propomos uma extensão das expressões regulares, que chamamos de expressões recursivas, como apoio à definição de um subconjunto das linguagens sem contexto. Assim, o objetivo do nosso trabalho é fornecer operadores simples para permitir definições de linguagens que sejam as mais próximas possíveis das linguagens sem contexto.

Oficinas Comuns e Consórcio de Doutorado do ADBIS, TPDL e EDA — 2020

The European Conference on Object-Oriented Programming (ECOOP)

Consultas de caminho sem contexto (CFPQ) são amplamente utilizadas na análise de dados estruturados em grafos em diferentes áreas. É crucial que se desenvolvam algoritmos de CFPQ altamente eficientes, porque tipicamente, o tamanho dos dados de entrada é grande. Mostramos como reduzir a avaliação de CFPQ à solução de sistemas de equações de matrizes sobre R — um problema para o qual existem soluções de alto desempenho. Também demonstramos a aplicabilidade da nossa abordagem à análise de dados no mundo real.

Anais do Congresso Internacional de Gerenciamento de Dados da ACM/SIGMOD de 2020

Este artigo tem o objetivo de apresentar uma modificação do algoritmo de Valiant. A principal vantagem dessa modificação é a possibilidade de dividir a tabela de parsing em camadas sucessivamente computadas de submatrizes disjuntas, em que cada submatriz de cada camada pode ser processada de forma independente. Além disso, nossa abordagem pode ser facilmente adaptada ao problema de correspondência de strings.

Proceedings of the Institute for System Programming

Um estudo recente mostrou que é limitada a aplicabilidade dos algoritmos de consultas de caminhos sem contexto (CFPQ) com semântica de consultas relacionais integrada em bancos de dados de grafos, por causa do baixo desempenho e alto consumo de memória das soluções existentes. Neste artigo, implementamos um algoritmo de CFPQ baseado em matrizes, que usa bibliotecas apropriadas de álgebra linear de alto desempenho, e integramos esse algoritmo a um banco de dados de grafos RedisGraph. Também apresentamos um novo algoritmo de CFPQ, com semântica de consulta de caminho único, que permite encontrar e extrair um caminho para cada par de nós. Finalmente, fornecemos uma avaliação dos nossos algoritmos para ambas as semânticas, mostrando que a implementação de CFPQ baseada em matrizes em bancos de dados RedisGraph tem desempenho suficiente para análise de dados no mundo real.

GRADES-NDA'20: Anais da 3ª Oficina Internacional Conjunta de Experiências e Sistemas de Gerenciamento de Dados de Grafos (GRADES) e Estatísticas de Dados de Redes (NDA)

41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020)

41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020)

Ao mesmo tempo que a utilização de GPUs permite acelerar computações por ordens de magnitude, o gerenciamento de memória continua sendo o gargalo que costuma tornar um desafio atingir o desempenho desejado. Daí resulta o aproveitamento de diferentes otimizações de memória, para tornar o uso desta mais eficaz. Propomos uma abordagem do gerenciamento automatizado de memória através da avaliação parcial, uma técnica de transformação de programas que permite que os acessos aos dados sejam pré-computados, otimizados e incluídos no código, poupando transações de memória. Uma avaliação empírica da nossa abordagem mostra que o programa transformado pode ser até 8 vezes mais eficiente que o original, no caso da implementação ingênua de um algoritmo de correspondência de padrões de strings em CUDA C.

PPoPP '20: Anais do 25º Simpósio da ACM SIGPLAN sobre os Princípios e a Prática da Programação Paralela

Anais do ISP RAS

Sabe-se que a consulta de caminhos com gramáticas conjuntivas não pode ser decidida. Existe um algoritmo de consulta de caminhos com gramáticas conjuntivas lineares que fornece uma superaproximação do resultado, mas não existia um algoritmo para gramáticas conjuntivas arbitrárias. Propomos o primeiro algoritmo de consulta de caminhos com gramáticas conjuntivas arbitrárias. O algoritmo proposto é baseado em matrizes e permite aplicar técnicas de computação em GPGPUs e outras otimizações a operações com matrizes, de forma eficiente.

Programming and Computer Software

BMC Bioinformatics

Anais do 19º Congresso Internacional de Métodos Formais em Projetos Assistidos por Computador — FMCAD 2019

33rd European Conference on Object-Oriented Programming (ECOOP 2019)

Um algoritmo recentemente proposto, baseado na multiplicação de matrizes, para consultas de caminhos sem contexto (CFPQ), transfere as partes mais críticas em termos de desempenho para multiplicações de matrizes booleanas. Assim, é possível conseguir um alto desempenho do CFPQ usando hardware e software paralelos modernos. Neste artigo, damos os resultados de uma comparação empírica do desempenho de diferentes implementações deste algoritmo, tanto com dados do mundo real quanto com dados sintéticos dos piores casos.

Anais da 2ª Oficina Internacional Conjunta de Experiências e Sistemas de Gerenciamento de Dados de Grafos (GRADES) e Estatísticas de Dados de Redes (NDA)

O teorema de Bar-Hillel diz que linguagens sem contexto são fechadas sob uma interseção com um conjunto regular. Esse teorema tem uma prova construtiva e, portanto, oferece uma justificativa formal da correção de algoritmos para as aplicações mencionadas acima. Assim, a mecanização do teorema de Bar-Hillel é ao mesmo tempo um resultado fundamental da teoria formal da linguagem e uma base para a implementação certificada de algoritmos para aplicações. Neste artigo, apresentamos a prova mecanizada do teorema de Bar-Hillel no Coq.

Logic, Language, Information, and Computation

Propomos uma maneira de combinar gramáticas formais e redes neurais artificiais para o processamento de sequências biológicas. As gramáticas formais codificam a estrutura secundária da sequência e as redes neurais lidam com as mutações e o ruído. Diferentemente do método clássico, no qual se usam gramáticas probabilísticas para modelar a estrutura secundária, propomos usar gramáticas arbitrárias (não probabilísticas), o que simplifica a criação de gramáticas. Em vez de modelarmos a estrutura da sequência inteira, criamos uma gramática que só descreve as características da estrutura secundária. Em seguida, usamos parsing baseado em matrizes para extrair as características; o fato de que se pode derivar alguma substring de algum ponto não terminal é, em si, uma característica. Depois disso, usamos uma rede neural densa para processar as características.

Anais do 12º Congresso Conjunto Internacional de Sistemas e Tecnologias de Engenharia Biomédica — BIOINFORMATICS

Um dos problemas da análise de dados de grafos é a consulta de caminhos específicos. Essas consultas geralmente são efetuadas através de uma gramática formal que descreve a rotulação permitida das bordas dos caminhos. Diz-se que uma consulta de caminho é calculada através de uma semântica de consultas relacionais quando ela é avaliada na terna (A,v1,v2) de modo que haja um caminho de v1 to v2 em que os rótulos em suas bordas formem uma string que possa ser derivada do A não terminal. Embora se saiba que consultas de caminhos usando semântica relacional de consultas e gramáticas booleanas não podem ser decididas, neste artigo propomos um algoritmo de consulta de caminhos em grafos acíclicos que usa semântica relacional de consultas e gramáticas booleanas, mas faz uma aproximação da solução exata. Para conseguir um desempenho melhor em comparação com um algoritmo ingênuo, as classes de grafos consideradas foram limitadas apenas a grafos acíclicos.

Proceedings of the Institute for System Programming

Anais da Oficina de miniKanren e Programação Relacional de 2019

SEIM-19

Anais Preliminares do 13º Colóquio de Primavera/Verão de Jovens Pesquisadores em Engenharia de Software (SYRCoSE 2019), 29 a 31 de maio de 2019 — Saratov, Federação Russa

Anais da Oficina de miniKanren e Programação Relacional de 2019

Anais da Oficina de miniKanren e Programação Relacional de 2019

Programming and Computer Software

Resumo ampliado no TyDe 2018 (no ICFP).

A integração transparente de uma linguagem específica de um domínio para a especificação de consultas de caminhos sem contexto (CFPQs) em uma linguagem de programação de uso geral e a verificação estática de erros nas consultas podem simplificar muito o desenvolvimento de aplicações usando CFPQs. LINQ e ORM podem ser usados nessa integração, mas eles têm problemas de flexibilidade: a decomposição de consultas e a reutilização de subconsultas são desafiadoras. Uma adaptação da técnica de combinadores de parsers para a consulta de caminhos pode resolver esses problemas. Os combinadores convencionais de parsers processam uma entrada linear e apenas a biblioteca Trails sabidamente aplica essa técnica na consulta de caminhos. Demonstramos que é possível criar combinadores gerais de parsers para CFPQ com suporte a gramáticas arbitrárias sem contexto e grafos de entrada arbitrários. Implementamos uma biblioteca desses combinadores de parsers e mostramos que ela pode ser aplicada em tarefas realistas.

Anais do 9º Simpósio Internacional ACM SIGPLAN sobre Scala

NTV SPbSTU

GRADES-NDA'18: Anais da 1ª Oficina Internacional Conjunta de Experiências e Sistemas de Gerenciamento de Dados de Grafos (GRADES) e Estatísticas de Dados de Redes (NDA)

18th International Symposium on Trends in Functional Programming

Anais do 20º Simpósio Internacional sobre os Princípios e a Prática da Programação Declarativa

Anais do ML/OCAML 2016

40th ACM/IEEE International Conference on Software Engineering, ICSE 2018

NTV SPbSTU

Existem várias soluções para CFPQ, mas fornecer uma representação estrutural do resultado da consulta que seja prática para o processamento e a depuração de respostas ainda é um problema sem solução. Neste artigo, propomos uma técnica de parsing de grafos que permite construir uma representação dessas, com relação a uma determinada gramática, para gramáticas e grafos arbitrários sem contexto, em tempo e espaço polinomiais. O algoritmo proposto é baseado em um algoritmo generalizado de parsing LL, enquanto as soluções anteriores eram baseadas principalmente nos algoritmos CYK ou Earley, e isso reduz a complexidade de tempo em alguns casos.

Anais do 13º Congresso de Engenharia de Software da Europa Central e Oriental na Rússia (CEE-SECR '17)

Anais do ISP RAS

arXiv

The European Conference on Object-Oriented Programming (ECOOP)

Anais da Oficina ACM SIGPLAN sobre Avaliação Parcial e Manipulação de Programas — 2017

St. Petersburg State Polytechnical University Journal. Computer Science. Sistemas de Telecomunicações e Controle

Izvestia vuzov. North Caucasus Region. Technical Sciences, 2017, Nº 4, páginas 5-12

Proceedings of the Institute for System Programming

arXiv

Apresentamos uma técnica de análise sintática de um conjunto regular de strings de entrada. Este problema é relevante para a análise de linguagens de strings incorporadas, quando um programa hospedeiro gera orações na linguagem incorporada durante a execução. Nossa técncia é baseada em uma generalização do algoritmo RNGLR, que permite inerentemente construir uma representação finita de uma floresta de parsing para um conjunto regularmente aproximado de strings de entrada. Essa representação também pode ser utilizada na análise semântica e em transformações nos contextos da reengenharia, manutenção do código, compreensão de programas, etc. A abordagem em questão implementa parsing relaxado: strings não reconhecidas no conjunto de aproximação são ignoradas, sem a detecção de erros.

Perspectives of System Informatics

Systems and Means of Informatics

META 2016 — 5ª Oficina Internacional Valentin Turchin sobre Metacomputação

SEIM-16

NTV SPbSTU 4 (224)

Systems and Means of Informatics

Science of Computer Programming

Anais do 11º Congresso de Engenharia de Software da Europa Central e Oriental na Rússia

Anais do 9º Congresso Internacional Memorial Andrei Ershov de Perspectivas em Informática de Sistemas

Anais do 10º Congresso de Engenharia de Software da Europa Central e Oriental na Rússia — 2014

Anais do 10º Congresso de Engenharia de Software da Europa Central e Oriental na Rússia

Anais do 9º Congresso de Engenharia de Software da Europa Central e Oriental na Rússia

Oficina de Aprendizado de Máquina

Anais do Simpósio Leste-Oeste sobre Projetos e Testes — 2010

Anais do 6º Congresso Internacional Memorial Andrei Ershov de Perspectivas em Informática de Sistemas

Oficina de Programação de Múltiplos Paradigmas com Linguagens Orientadas a Objetos

System Informatics

System Programming

System Programming

Anais do Congresso Europeu de Manutenção e Reengenharia de Software, CSMR 995802, pp. 177–185

Anais do 4º Congresso Internacional Memorial Andrei Ershov de Perspectivas em Informática de Sistemas

Automated Reengeneering of Programs, Saint Petersburg