1 Search Results for "Huet, Gérard"

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-dev.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}
}
  • Refine by Author
  • 1 Huet, Gérard

  • Refine by Classification

  • Refine by Keyword
  • 1 Computation
  • 1 Deduction
  • 1 Foundations
  • 1 Programming
  • 1 Proofs

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2016

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact