JFLAs 2014Articles acceptésFormal verification in Coq of program properties involving the global state effect Vérification de programmes C concurrents avec Cubicle : Enfoncer les barrières What could Coq do for Database Software? ---A Progress Report Exécution efficace de programmes ReactiveML Unification des couleurs dans un $\lambda$-calcul polychrome Une sémantique statique pour MongoDB Réseaux de Kahn à rafales et horloges entières Pretty-big-step-semantics-based Certified Abstract Interpretation Comment un chameau peut-il écrire un journal ? De la KAM avec un Processus dâOrdre SupeÌrieur Analyse de dépendances et correction des réseaux de preuve Nécessité faite loi : de la réduction linéaire de tête à l'évaluation paresseuse Exposés courtsTraduction prouvée de HOL4 vers le premier ordre. Réflexions sur l'écriture de parsers binaires robustes et présentation de la solution Parsifal. Le petit guide du bouturage. NB: le classement correspond à l'ordre de dépot sur easychair, il n'est pas significatif. |