报告题目: |
Introduction to Agda language and system |
报告人: |
KINOSHITA Yoshiki, |
|
Dr. National Institute of Advanced Industrial
Science and Technology, Japan
|
报告时间: |
2009-04-24 10:30 |
报告地点: |
Tsinghua University, FIT Building, Room 3-125 |
主办单位: |
清华大学软件学院 |
简介: |
Formal Methods for Embedded Systems (FORMES) series seminars
FORMES seminar, Fri, 24 Apr 2009 10:30
Title: Introduction to Agda language and system
Venue Tsinghua University, FIT Building, Room 3-125
Speaker Dr. KINOSHITA Yoshiki, National Institute of Advanced Industrial
Science and Technology, Japan
I shall give a short introduction to Agda language and system, which is
developped in Chalmers University of Technology and AIST. Agda language is,
like Coq, based on Constructive Type Theory, so it can be seen as a functional
programming language equipped with dependent types as well as description
language for logical formulae and their proofs. I shall first explain Agda as a
programming language, especially about its dependent types which are called
datatypes (corresponding to so-called sigma types) and record types (corr. so-
called pi types). I shall then show Agda as a proof system and how logical
formulae and proofs are embedded in Agda. The way of embedding logic in Agda is
not unique; the one I shall use is a typical “shallow” embedding. The time
permitting, I shall also mention about the system which processes Agda language.
|
|
