DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2016.3

Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization

Authors: Gérard Huet

Published in: LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Abstract

We describe experiments in teaching fundamental informatics notions around mathematical structures for formal concepts, and effective algorithms to manipulate them. The major themes of lambda-calculus and type theory served as guides for the effective implementation of functional programming languages and higher-order proof assistants, appropriate for reflecting the theoretical material into effective tools to represent constructively the concepts and formally certify the proofs of their properties. Progressively, a literate programming and proving style replaced informal mathematics in the presentation of the material as executable course notes. The talk will evoke the various stages of (in)completion of the corresponding set of notes along the years, and tell how their elaboration proved to be essential to the discovery of fundamental results.

Cite as

Gérard Huet. Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{huet:LIPIcs.FSCD.2016.3,
  author =	{Huet, G\'{e}rard},
  title =	{{Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{3:1--3:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Kesner, Delia and Pientka, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.3},
  URN =		{urn:nbn:de:0030-drops-60020},
  doi =		{10.4230/LIPIcs.FSCD.2016.3},
  annote =	{Keywords: Foundations, Computation, Deduction, Programming, Proofs}
}

Search Results

Documents authored by Huet, Gérard

Teaching Foundations of Computation and Deduction Through Literate Functional Programming and Type Theory Formalization

Abstract

Cite as

Thanks for your feedback!

Could not send message