Home » forums » LtU Forum

Certified Programming with Dependent Types: home stretch!

For the last few years, I've been working on Certified Programming with Dependent Types, a book giving a pragmatic introduction to the Coq proof assistant. The drafts have been available for free online, and future versions should be as well; but I'm also working toward a traditional print version from MIT Press.

I've recently finished the last non-trivial content changes that I've had planned, so I write to you to ask for your help in finding the last mistakes and opportunities for improvement! Once everything is in good shape, I can move forward with traditional publication.

There are a few categories of known issues. One is font choice and other typesetting; this is coming from coqdoc, Coq's documentation generation program, and I expect to need to jump into the coqdoc source code to an extent, to get everything looking pretty without excessive countermeasures in the book source code.

Where I could especially use help is finding appropriate citations to research papers and so on. There are few subjects that I'm already looking for the right citations on, and I figure LtU is a great place to find people who have favorites in these categories. So, could you please let me know if you have a citation to recommend for any of the following?

  • the concept of continuation and/or continuation-passing style
  • the concept of unification
  • infinite data structures in Haskell
  • Haskell "deriving" clauses
  • some introduction to logic programming, to cite in lieu of going into full detail on the usual foundations of the paradigm

I'll also appreciate advice on any other points in the text that you think deserve citations, and I'll appreciate suggestions the most if they come with suggested citation targets. :)

And any other finding of typos, confusing prose, and so on will be much appreciated! You can e-mail me or reply to this post, as seems appropriate.

Thanks in advance! I'm looking forward to getting the book out there.

By Adam Chlipala at 2012-04-16 22:54 | LtU Forum | previous forum topic | next forum topic | other blogs | 127050 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Citations

On the history of continuations, see Reynolds' paper "The Discoveries of Continuations".

Unification is due to Robinson, I think. Wikipedia claims the cite is: John Alan Robinson, "A Machine-Oriented Logic Based on the Resolution Principle", Communications of the ACM, 5:23–41, 1965.

By Sam Tobin-Hochstadt at Tue, 2012-04-17 01:15 | login or register to post comments

Thanks!

I'm now planning to use both of those.

By Adam Chlipala at Sun, 2012-04-22 19:50 | login or register to post comments

There is exactly one

There is exactly one sentence in the whole book that mentions certifications en passant. Of course I don't mind that because its a free and online book, I didn't order it on Amazon based on its title and it is possibly a great resource for learning another geek toy, but I wonder why the author has chosen it if he has nothing to say about the relationship between theorem provers and software certifications.

By Kay Schluehr at Tue, 2012-04-17 18:03 | login or register to post comments

Suggestion

May I respectfully suggest that you read it, and see whether or not it has anything to say about the relationship between theorem provers and software certifications?

By Paul Snively at Tue, 2012-04-17 20:38 | login or register to post comments

Using the terms like Adam

Using the terms like Adam Chlipala it becomes a tautology. Proving software correct by proving it correct using theorem provers. The motivation to do so could have been a "certification" as it is understood by every other engineer on the planet.

By Kay Schluehr at Wed, 2012-04-18 01:44 | login or register to post comments

What's a tautology?

The title of his book? How is it a proposition?

By Matt M at Wed, 2012-04-18 02:46 | login or register to post comments

Lost

Kay Schluehr: Using the terms like Adam Chlipala it becomes a tautology. Proving software correct by proving it correct using theorem provers. The motivation to do so could have been a "certification" as it is understood by every other engineer on the planet.

I'm confused. You're unhappy with the actually useful result, and would rather have a meaningless piece of paper?

By Paul Snively at Wed, 2012-04-18 15:42 | login or register to post comments

Me? I don't care either way.

Me? I don't care either way. Neither do I need software which follows some platonic ideal cultivated by a vanishing minority crowd, nor do I need products that pass through a certification process and can be sold only by gathering a meaningless piece of paper ( which coincidentally can be said about cash, which is also only needed as an enabler for something else ). O.K. occasionally those products are useful.

But there is at least a slight interest in the relationship between both. Why not extend the scope of professional activity and interest - and it doesn't get much further then this - by the former in service of the latter? Now it looks like someone has clarified those things but then no, he doesn't. He only used a term which is hijacked by his in-group. So may it be.

By Kay Schluehr at Thu, 2012-04-19 03:39 | login or register to post comments

OK

Kay Schluehr: Me? I don't care either way.

I don't believe you.

First of all, because you commented. But further...

Neither do I need software which follows some platonic ideal cultivated by a vanishing minority crowd...

Abject ignorance wrapped in condescension, proving that you do care and just don't like what you see.

...nor do I need products that pass through a certification process and can be sold only by gathering a meaningless piece of paper...

You might not, but others might. Why not develop for them and imbue that meaningless piece of paper with meaning?

But there is at least a slight interest in the relationship between both.

Then read the book and learn something.

Why not extend the scope of professional activity and interest - and it doesn't get much further then this - by the former in service of the latter?

Why do you presume Adam hasn't?

Now it looks like someone has clarified those things but then no, he doesn't.

How do you know he doesn't? From the available evidence, you did a global search for the word "certification" and came up empty, then decided to post here about something you claim not to care about, revealing that you didn't read the book, don't know what it's about, and/or can't see a connection to what you assumed the book was about.

He only used a term which is hijacked by his in-group.

As opposed to you hijacking the same term—which is perfectly well-understood in the formal methods community—for yours.

So may it be.

If this is actually how you feel, why didn't you take the opportunity to shut up?

By Paul Snively at Thu, 2012-04-19 04:46 | login or register to post comments

I should probably explain

I should probably explain what I mean by "certified" somewhere explicitly. It's not at all like certification as in common government regulation schemes. Rather, "certified" here means "formally verified," more or less.

By Adam Chlipala at Wed, 2012-04-18 01:19 | login or register to post comments

Gratitude

Adam Chlipala: It's not at all like certification as in common government regulation schemes. Rather, "certified" here means "formally verified," more or less.

And thank God for it.

By Paul Snively at Wed, 2012-04-18 15:43 | login or register to post comments

For data structures in Haskell...

...the useful keywords are "inverse limit construction", "limit-colimit coincidence", and less commonly, "bilimit-compact". As you know, the idea is that you can model general recursive types by means of sequences of approximations which are related by embedding-projection pairs.

The reference to Scott's paper is:

  • Scott, Dana. Continuous Lattices. 1971 Dalhousie Conference on Toposes, Algebraic Geometry and Logic. Lawvere, Bill, editor. Published in Lecture Notes in Mathematics, 274, Springer-Verlag, Berlin, pp. 97-136.

The modern approach to this is summarized in the following pair of references:

  • Smyth, Michael and Plotkin, Gordon. The Category-Theoretic Solution of Recursive Domain Equations. 1982. SIAM Journal on Computing, Volume 11, No. 4, pp. 761-783
  • Pitts, Andrew M. Relational Properties of Domains. 1996. Information and Computation, Volume 127, No. 2. pp. 66-90

However, Coq (being total) has a rather different semantics for its types. It does not have general recursive types, and inductive types (initial algebras) and coinductive types (final coalgebras) do not coincide, as they do in Haskell.

Applications of these ideas to programming date back to the work of the ADJ group (Goguen, Thatcher, Warner and Wright) on functorial semantics back in the 1970s, and the first first explicit application of coalgebra-as-coalgebra to PL dates to Peter Aczel's work on non-well-founded set theory to give denotational semantics for Milner's work on concurrency.

However, to my knowledge, the first treatment of codata as a functional programming technique in a recognizably modern form is in Hagino's PhD thesis

  • Hagino, Tatsuya. A Categorical Programming Language, 1987. PhD thesis, University of Edinburgh.

which was followed by the constructive algorithmics/squiggol/program calculation crowd developing and popularizing these ideas in Haskell programming. As a random example, see:

  • Gibbons, Jeremy and Jones, Geraint. The Under-appreciated Unfold, 1998. ICFP.
By neelk at Sun, 2012-04-22 22:31 | login or register to post comments