[Alta-Logic] Peripatetic Seminar: Chad Nester -- Tomorrow!

[Chad Nester]

Speaker: Chad Nester

Time and Date: Friday Nov 14th at 11am

Location: ICT 638

Abstract: In Hindley-Milner style languages, such as Haskell and ML, there
is a clear separation between types and values. In dependently typed
languages the distinction is less clear. Types can contain (depend on)
arbitrary values and appear as arguments and results of ordinary functions.
Additionally, the theory of dependent types provides a constructive
foundation for mathematics under a Martin-Löf style interpretation,
allowing dependently typed languages to serve as proof verification systems
in addition to programming languages. In this talk I will give a brief
introduction to the dependently typed language Agda, including examples of
some common dependent types, and some simple verified proofs in the system.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.ucalgary.ca/pipermail/alta-logic-l/attachments/20141113/bd74ba33/attachment.html