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

miniKanren est un langage intégré léger conçu pour les programmations logiques et relationnelles. La plupart de ses fonctionnalités très pratiques sont dérivées d'une stratégie de recherche originale, appelée recherche par entrelacement. La recherche par entrelacement contourne les méthodes conventionnelles de raisonnement sur la complexité et les performances des programmes logiques. Nous avons identifié un composant clé important, la planification, qui rend le raisonnement de miniKanren si différent, et présente une technique semi-automatique d'estimation de l'impact planifié via l'exécution symbolique pour une classe de logiciels raisonnablement étendue.

49e symposium de l'ACM SIGPLAN sur les principes des langages de programmation (POPL 2012)

Scientific and Technical Journal of Information Technologies, Mechanics and Optics

Syrcose'21

TFPIE-2021

Prix du meilleur article à OOPSLA'21

OOPSLA

Programming and Computer Software Journal

Nous présentons une nouvelle stratégie juste d'évaluation de conjonctions pour le langage de programmation relationnelle miniKanren. Contrairement aux conjonctions d'origines partant de la gauche, notre approche contrôle l'ordre d'exécution des conjonctions en fonction des propriétés intrinsèques des définitions de relations. Nous présentons à la fois l'étude formelle de la justesse des conjonctions et leur évaluation pratique, ce qui démontre des améliorations essentielles, aussi bien en termes de performances que de convergence.

SEIM-2021

ICPP-2021

Nous présentons une étude formelle de la sémantique pour le langage de programmation relationnelle miniKanren. Tout d'abord, nous formulons une sémantique dénotationnelle qui correspond au modèle Herbrand de programmes logiques définis. Ensuite, nous présentons la sémantique opérationnelle qui modélise l'entrelacement, la fonctionnalité distinctive de l'implémentation de miniKanren et prouvons son bien-fondé et son intégrité concernant la sémantique dénotationnelle. Notre développement est encadré par une spécification COQ, qui permet d'extraire un interpréteur de référence. Nous avons également dérivé une sémantique certifiée (et un interpréteur de référence) à partir de notre résultat principal pour la résolution SLD avec coupe et prouvons son bien-fondé.

Nous présentons une approche totalement déclarative de la synthèse d'implémentations de construction de filtrage par motif basée sur l'application de la programmation relationnelle, une forme spécifique de la programmation à logique de contrainte. Notre approche repose à la fois sur les représentations relationnelles de la sémantique du filtrage par motif et la sémantique d'un langage d'implémentation de niveau intermédiaire. Ce choix rend, en principe, notre approche très évolutive, car nous devons seulement modifier la sémantique de haut niveau pour synthétiser l'implémentation d'une nouvelle fonctionnalité de filtrage par motif. Notre évaluation porte sur plusieurs petits échantillons, extraits en partie de la documentation existante et démontre que notre framework est capable de synthétiser des implémentations optimales rapidement. L'évaluation approfondie sous contrainte que nous avons mené sur plusieurs références artificielles indique toutefois qu'il reste de nombreuses améliorations à apporter.

Les requêtes de chemin à contexte libre (CFPQ) prolongent les requêtes de chemin standard (RPQ) en permettant d'utiliser des grammaires à contexte libre en tant que contraintes pour les chemins. Des algorithmes de CFPQ sont développés activement, mais J. Kuijpers et al. ont récemment conclu que les algorithmes existants ne sont pas encore assez performants pour les applications de production. Par conséquent, le développement de nouveaux algorithmes pour CFPQ est justifié. Dans cet article, nous proposons un nouvel algorithme CFPQ qui repose sur des opérations algébriques linéaires, telles que le produit de Kronecker et les fermetures transitives, et gère les grammaires présentées comme des machines d'état récursives. Ainsi, l'algorithme proposé peut être implémenté au moyen de bibliothèques hautes performances et de matériel parallèle moderne. De plus, il évite la croissance de la grammaire, ce qui donne la possibilité d'optimiser les requêtes.

ADBIS 2020. Advances in Databases and Information Systems. Lecture Notes in Computer Science.

Les expressions régulières interviennent dans les chemins de propriétés SPARQL pour les requêtes portant sur les graphiques RDF. Cependant, les expressions régulières ne peuvent définir que la classe la plus limitée des langages, appelée « langages réguliers ». Les langages à contexte libre constituent une classe plus large qui recouvre tous les langages réguliers. Il n'existe pas d'expressions à contexte libre pour les définir, par conséquent il est nécessaire d'écrire des grammaires. Nous proposons une extension des expressions régulières, appelée « expressions récursives », pour accompagner la définition d'un sous-ensemble de langages à contexte libre. Ainsi, l'objectif de notre travail est de fournir des opérateurs simples permettant de définir des langages aussi proches que possible des langages à contexte libre.

ADBIS, TPDL et EDA Édition 2020 des ateliers communs et du consortium doctoral

The European Conference on Object-Oriented Programming (ECOOP)

La requête de chemin à contexte libre (CFPQ) intervient généralement dans l'analyse de données structurée par des graphiques dans différents domaines. Il est essentiel de développer des algorithmes ultra-efficaces pour les requêtes CFPQ, car les données en entrée sont généralement considérables. Nous démontrons comment ramener l'évaluation de la requête CFPQ à la résolution d'équations matricielles sur R, un problème pour lequel il existe des solutions hautes performances. D'autre part, nous démontrons que notre approche peut s'appliquer à l'analyse de données dans un environnement de production.

Compte rendu de l'édition 2020 de la conférence internationale sur la gestion des données de l'ACM SIGMOD

Cet article a pour objectif de présenter l'article de modification de Valiant, dont le principal avantage réside dans la possibilité de diviser la table d'analyse en couches de calcul successives de sous-matrices non liées, où chaque sous-matrice de la couche peut être traitée de façon indépendante. De plus, notre approche peut être facilement adaptée au problème de mise en correspondance des chaînes.

Compte rendu de l'Institute for System Programming

Une étude récente a démontré que l'intérêt d'algorithmes de requête de chemin à contexte libre (CFPQ) avec une sémantique de requête relationnelle intégrée dans les bases de données graphiques est limité, en raison de faibles performances et de la forte consommation de mémoire des solutions existantes. Dans le cadre de ce travail, nous implémentons un algorithme CFPQ basé sur une matrice en utilisant des bibliothèques hautes performances adaptées à l'algèbre linéaire et l'intégrons avec la base de données graphique RedisGraph. D'autre part, nous avons introduit un nouvel algorithme CFPQ avec une sémantique de requête à chemin unique qui permet d'extraire un chemin trouvé pour chaque paire de nœuds. Enfin, nous procédons à l'évaluation de nos algorithmes pour les deux sémantiques, ce qui démontre que l'implémentation CFPQ basée sur matrice pour la base de données Redis-Graph est suffisamment performante pour l'analyse des données en temps réel.

GRADES-NDA'20 : compte rendu du 3e atelier international sur les systèmes et expériences de gestion des données graphiques (GRADES) et analyse des données en réseau (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)

Si l'utilisation d'un processeur graphique permet d'accélérer considérablement les calculs, la gestion de la mémoire reste un goulot d'étranglement qui rend souvent difficile l'obtention des performances voulues. Par conséquent, différentes optimisations de mémoire ont été utilisées pour optimiser la mémoire exploitée. Nous proposons une approche d'automatisation de la mémoire s'appuyant sur une évaluation partielle, une technique de transformation des programmes qui permet de pré-calculer les accès aux données, de les optimiser et de les intégrer dans le code, ce qui réduit les transactions en mémoire. Une évaluation empirique de notre approche démontre que le programme transformé pourrait être 8 fois plus efficace que le programme d'origine dans le cas de l'implémentation de l'algorithme naïf de filtrage par motifs de chaînes CUDA C.

PPoPP '20 : Compte rendu du 25e symposium de l'ACM SIGPLAN sur les principes et la pratique de la programmation parallèle

Compte-rendu d'ISP RAS

Les requêtes de chemin avec grammaires conjonctives sont connues pour être indécidables. Il existe un algorithme de requête sur les chemins utilisant des grammaires conjonctives qui produit une sur-approximation du résultat, mais il n'y a pas d'algorithme pour les grammaires conjonctives arbitraires. Nous proposons le premier algorithme de requête de chemin gérant des grammaires conjonctives arbitraires. L'algorithme proposé a une base matricielle et nous permet d'appliquer efficacement les techniques de calcul GPGPU aux opérations matricielles.

Programming and Computer Software

BMC Bioinformatics

Compte rendu de la 19e conférence internationale sur les méthodes formelles de conception assistée par ordinateur, FMCAD 2019

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

Un algorithme basé sur la multiplication matricielle proposé récemment pour les requêtes de chemin à contexte libre (CFPQ) délègue les éléments ayant le plus d'effet sur les performances aux matrices booléennes de multiplication. Ainsi, il est possible d'obtenir un algorithme CFPQ ultra-performant au moyen de matériels et logiciels parallèles modernes. Vous trouverez dans cet article les résultats de la comparaison empirique des performances de différentes implémentations de cet algorithme, à la fois pour les données en temps réel et synthétiques pour les cas les plus graves.

Compte rendu du 2e atelier international sur les systèmes et expériences de gestion des données graphiques (GRADES) et analyse des données en réseau (NDA)

Le théorème Bar-Hillel affirme que les langages à contexte libre sont fermés par l'intersection avec un ensemble régulier. Ce théorème inclut une preuve constructive et par conséquent assure une justification formelle d'exactitude des algorithmes pour les applications mentionnées ci-dessus. La mécanisation du théorème de Bar-Hillel, par conséquent, est à la fois le résultat fondamental d'une théorie de langage formel et une base d'implémentation certifiée des algorithmes pour les applications. Dans le cadre de ce travail, nous présentons la preuve mécanisée du théorème Bar-Hillel dans Coq.

Logic, Language, Information, and Computation

Nous proposons une possibilité de combinaison des grammaires formelles et des réseaux neuronaux artificiels pour le traitement des séquences biologiques. Les grammaires formelles codent la structure secondaire de la séquence et les réseaux neuronaux gèrent les mutations et le bruit. Par opposition à la méthode classique, où les grammaires probabilistes interviennent pour la modélisation de structure secondaire, nous proposons d'utiliser des grammaires arbitraires (non probabilistes), ce qui simplifie la création de grammaires. Au lieu de modéliser la structure de l'ensemble de la séquence, nous avons créé une grammaire décrivant uniquement les fonctionnalités de la structure secondaire. Ensuite, nous utilisons l'analyse à base matricielle pour extraire des fonctionnalités : le fait que certaines sous-chaînes soient dérivées depuis un élément non terminal est caractéristique. Ensuite, nous utilisons un réseau neuronal dense pour traiter les fonctionnalités.

Compte rendu de la 12e conférence internationale sur les systèmes et technologies d'ingénierie biomédicale - BIO-INFORMATIQUE

L'un des problèmes de l'analyse des données graphiques réside dans les requêtes portant sur des chemins spécifiques. Ces requêtes sont généralement exécutées au moyen d'une grammaire formelle qui décrit l'étiquetage possible des arêtes des chemins. Une requête de chemin est dite comme ayant été calculée avec une sémantique de requête relationnelle quand elle est évaluée en triple (A,v1,v2), de sorte qu'il y a un chemin de v1 à v2, et que les étiquettes sur les arêtes de ce chemin forment un chaîne dérivable depuis le A non terminal. Nous nous concentrons sur les langages booléens utilisant des grammaires booléennes pour décrire l'étiquetage des chemins. Bien que les requêtes de chemin recourant à une sémantique de requête relationnelle et les grammaires booléennes soient connues comme indécidables, dans cet article, nous proposons un algorithme de requête sur le chemin pour les graphiques acycliques utilisant des sémantiques de requêtes relationnelles, ainsi que des grammaires booléennes et faisons une approximation de la solution exacte. Pour obtenir de meilleures performances par rapport à l'algorithme naïf, les classes prises en compte des graphiques ont été limitées à des graphiques acycliques.

Compte rendu de l'Institute for System Programming

Compte rendu de l'édition 2019 de l'atelier consacré au miniKanren et à la programmation relationnelle

SEIM-19

Compte rendu préliminaire du 13e colloque de printemps/été des jeunes chercheurs en ingénierie logicielle (SYRCoSE 2019), 29-31 mai 2019 – Saratov, Fédération de Russie

Compte rendu de l'édition 2019 de l'atelier consacré au miniKanren et à la programmation relationnelle

Compte rendu de l'édition 2019 de l'atelier consacré au miniKanren et à la programmation relationnelle

Programming and Computer Software

Abstract étendu à TyDe 2018 (à ICFP).

L'intégration transparente d'un langage propre au domaine pour la spécification de requêtes de chemin à contexte libre (CFPQ) dans un langage de programmation généraliste, ainsi que la vérification statique d'erreurs dans les requêtes peut simplifier considérablement le développement d'applications utilisant les algorithmes CFPQ. LINQ et ORM peuvent être utilisés pour l'intégration, mais ils posent des problèmes de flexibilité : la décomposition des requêtes et la réutilisation des sous-requêtes sont difficiles. L'adaptation d'une technique de combinateurs d'analyseurs pour les requêtes de chemin pourrait résoudre ces problèmes. Les combinateurs d'analyseurs conventionnels traitent une entrée linéaire, et seule la bibliothèque Trails est connue comme appliquant cette technique aux requêtes de chemin. Nous démontrons qu'il est possible de créer des combinateurs d'analyseurs généralistes pour CFPQ qui prennent en charge les grammaires arbitraires à contexte libre, ainsi que les graphiques d'entrée arbitraires. Nous avons implémenté une bibliothèque de ces combinateurs d'analyseurs et démontré qu'elle était utilisable pour des tâches de production.

Compte rendu du 9e symposiuym annuel de l'ACM SIGPLAN sur Scala

NTV SPbSTU

GRADES-NDA '18 : compte rendu du 1er atelier international sur les systèmes et expériences de gestion des données graphiques (GRADES) et analyse des données en réseau (NDA) de l'ACM SIGMOD

18th International Symposium on Trends in Functional Programming

Compte rendu du 20e symposium international sur les principes et la pratique de la programmation parallèle

Compte rendu ML/OCAML 2016

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

NTV SPbSTU

Il existe plusieurs solutions pour CFPQ, mais comment fournir une représentation structurelle du résultat de la requête qui soit utile pour le traitement des réponses et le débogage reste un problème ouvert. Dans cet article, nous proposons une technique d'analyse des graphiques qui permet de créer cette représentation par rapport à une grammaire donnée en temps polynomial, ainsi qu'un espace pour une grammaire à contexte libre et des graphiques arbitraires. L'algorithme proposé est basé sur l'algorithme d'analyse LL généralisé, tandis que les solutions précédentes reposent principalement sur les algorithmes CYK ou Earley, qui réduisent la complexité temporelle dans certains cas.

Compte rendu de la 13e conférence d'ingénierie logicielle en Europe centrale et orientale organisée en Russie (CEE-SECR ’17)

Compte-rendu d'ISP RAS

arXiv

The European Conference on Object-Oriented Programming (ECOOP)

Compte rendu de l'édition 2017 de l'atelier sur l'évaluation partielle et la manipulation des programmes de l'ACM SIGPLAN

St. Petersburg State Polytechnical University Journal. Computer Science. Systèmes de télécommunications et de contrôle

Izvestia vuzov. North Caucasus Region. Technical Sciences, 2017, N° 4, pages 5-12

Compte rendu de l'Institute for System Programming

arXiv

Nous présentons une technique d'analyse de la syntaxe pour un ensemble standard de chaînes d'entrée. Ce problème concerne également l'analyse des langages intégrés dans les chaînes lorsqu'un programme hôte génère des clauses de langage intégré lors de l'exécution. Notre technique repose sur la généralisation de l'algorithme RNGLR qui, de façon inhérente, nous permet de construire une représentation finie de la forêt d'analyse pour ensemble à approximation régulière de chaînes d'entrée. Cette représentation peut être utilisée de façon plus poussée pour l'analyse de la sémantique et les transformations dans le contexte de la réingénierie, de la maintenance du code, de la compréhension des programmes, etc. L'approche en question implémente l'analyse relaxée : les chaînes non reconnues dans l'ensemble d'approximation sont ignorées, sans détection des erreurs.

Perspectives of System Informatics

Systems and Means of Informatics

META 2016 Cinquième atelier international Valentin Turchin sur le métacalcul

SEIM-16

NTV SPbSTU 4 (224)

Systems and Means of Informatics

Science of Computer Programming

Compte rendu de la 11e conférence d'ingénierie logicielle en Europe centrale et orientale organisée en Russie

Compte rendu de la 9e conférence internationale du Mémorial à Andrei Ershov sur les perspectives de l'informatique système

Compte rendu de la 10e conférence d'ingénierie logicielle en Europe centrale et orientale organisée en Russie (2014)

Compte rendu de la 10e conférence d'ingénierie logicielle en Europe centrale et orientale organisée en Russie

Compte rendu de la 9e conférence d'ingénierie logicielle en Europe centrale et orientale organisée en Russie

Atelier de ML

Compte rendu de l'édition 2010 du symposium sur la conception et les tests est-ouest

Compte rendu de la 6e conférence internationale du Mémorial à Andrei Ershov sur les perspectives de l'informatique système

Atelier sur la programmation à paradigmes multiples pour les langages orientés objet

System Informatics

System Programming

System Programming

Compte rendu de la conférence européenne sur la maintenance logicielle et la réingénérie, CSMR 995802, pp. 177-185

Compte rendu de la 4e conférence internationale du Mémorial à Andrei Ershov sur les perspectives de l'informatique système

Automated Reengeneering of Programs, Saint Petersburg