Interaction trees: representing recursive and impure programs in Coq - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Proceedings of the ACM on Programming Languages Année : 2020

Interaction trees: representing recursive and impure programs in Coq

Li-Yao Xia
  • Fonction : Auteur
Computer Science Department
Yannick Zakowski
Computer Science Department
Paul He
  • Fonction : Auteur
Computer Science Department
Chung-Kil Hur
  • Fonction : Auteur
Seoul National University [Seoul]
Gregory Malecha
  • Fonction : Auteur
BedRock Systems Inc.
Benjamin Pierce
  • Fonction : Auteur
Computer Science Department
Steve Zdancewic
Computer Science Department

Domaines

Langage de programmation [cs.PL]

Yannick Zakowski  : Connectez-vous pour contacter le contributeur

https://hal.science/hal-03105140

Soumis le : dimanche 10 janvier 2021-20:02:14

Dernière modification le : jeudi 16 février 2023-11:24:09

Consulter le texte intégral

Dates et versions

hal-03105140 , version 1 (10-01-2021)

Identifiants

Citer

Li-Yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, et al.. Interaction trees: representing recursive and impure programs in Coq. Proceedings of the ACM on Programming Languages, 2020, 4 (POPL), pp.1-32. ⟨10.1145/3371119⟩. ⟨hal-03105140⟩

Exporter

BibTeX XML-TEI Dublin Core DC Terms EndNote DataCite
42 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More