View in EDS PDF Full Text

Correct and Complete Type Checking and Certified Erasure for Coq, in Coq.

Saved in:
Bibliographic Details
Title: Correct and Complete Type Checking and Certified Erasure for Coq, in Coq.
Authors: Sozeau, Matthieu1 (AUTHOR) matthieu.sozeau@inria.fr, Forster, Yannick2 (AUTHOR) yannick.forster@inria.fr, Lennon-Bertrand, Meven3 (AUTHOR) mgapb2@cam.ac.uk, Nielsen, Jakob4 (AUTHOR) jakob.botsch.nielsen@gmail.com, Tabareau, Nicolas1 (AUTHOR) nicolas.tabareau@inria.fr, Winterhalter, Théo5 (AUTHOR) theo.winterhalter@inria.fr
Source: Journal of the ACM. Feb2025, Vol. 72 Issue 1, p1-74. 74p.
Database: Business Source Ultimate
FullText Links:
  – Type: pdflink
Text:
  Availability: 0
Header DbId: bsu
DbLabel: Business Source Ultimate
An: 182534096
AccessLevel: 2
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Correct and Complete Type Checking and Certified Erasure for Coq, in Coq.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Sozeau%2C+Matthieu%22">Sozeau, Matthieu</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> matthieu.sozeau@inria.fr</i><br /><searchLink fieldCode="AR" term="%22Forster%2C+Yannick%22">Forster, Yannick</searchLink><relatesTo>2</relatesTo> (AUTHOR)<i> yannick.forster@inria.fr</i><br /><searchLink fieldCode="AR" term="%22Lennon-Bertrand%2C+Meven%22">Lennon-Bertrand, Meven</searchLink><relatesTo>3</relatesTo> (AUTHOR)<i> mgapb2@cam.ac.uk</i><br /><searchLink fieldCode="AR" term="%22Nielsen%2C+Jakob%22">Nielsen, Jakob</searchLink><relatesTo>4</relatesTo> (AUTHOR)<i> jakob.botsch.nielsen@gmail.com</i><br /><searchLink fieldCode="AR" term="%22Tabareau%2C+Nicolas%22">Tabareau, Nicolas</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> nicolas.tabareau@inria.fr</i><br /><searchLink fieldCode="AR" term="%22Winterhalter%2C+Théo%22">Winterhalter, Théo</searchLink><relatesTo>5</relatesTo> (AUTHOR)<i> theo.winterhalter@inria.fr</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Journal+of+the+ACM%22">Journal of the ACM</searchLink>. Feb2025, Vol. 72 Issue 1, p1-74. 74p.
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=bsu&AN=182534096
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1145/3706056
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 74
        StartPage: 1
    Titles:
      – TitleFull: Correct and Complete Type Checking and Certified Erasure for Coq, in Coq.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Sozeau, Matthieu
      – PersonEntity:
          Name:
            NameFull: Forster, Yannick
      – PersonEntity:
          Name:
            NameFull: Lennon-Bertrand, Meven
      – PersonEntity:
          Name:
            NameFull: Nielsen, Jakob
      – PersonEntity:
          Name:
            NameFull: Tabareau, Nicolas
      – PersonEntity:
          Name:
            NameFull: Winterhalter, Théo
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 02
              Text: Feb2025
              Type: published
              Y: 2025
          Identifiers:
            – Type: issn-print
              Value: 00045411
          Numbering:
            – Type: volume
              Value: 72
            – Type: issue
              Value: 1
          Titles:
            – TitleFull: Journal of the ACM
              Type: main
ResultId 1