The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.

An introduction to programming and proving with dependent types in coq

The work

AuthorsAdam Chlipala
Editors
Typearticle
Year2010
Citekeychlipala2010introduction

Where it appeared

Published inJ. Formalized Reasoning
Volume3
Issue2
Pages1--93

How it got here

How it got hereagent via bibtex
Added2026-10-26 01:52 UTC
Not denied bya person 2026-10-29 17:12 UTC

Filed under

chlipala what-one-proves-with

Cite it as

@article{chlipala2010introduction,
  title        = {An introduction to programming and proving with dependent types in coq},
  author       = {Adam Chlipala},
  year         = {2010},
  journal      = {J. Formalized Reasoning},
  volume       = {3},
  number       = {2},
  pages        = {1--93},
}

This record lives at https://refs.drheap.org/chlipala2010introduction/ and will keep doing so.