Deprecated : The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Inductive and inductive-recursive definitions in type theory
Inductive sets and families in Martin-Löf's type theory and their
set-theoretic semantics , in Logical Frameworks, 1991, editors
Gerard Huet and Gordon Plotkin, pp 280-306, Prentice Hall.
Inductive Families , in Formal Aspects of Computing 6, 1994,
pp 440-465.
Inductive definitions and type theory an introduction (preliminary version) (with Thierry Coquand), pp 60 - 76 in
Foundation of Software Technology and Theoretical Computer Science: 14th Conference Madras, India, December 15-17, 1994 Proceedings. Editors: P. S. Thiagarajan, Springer LNCS 880, 1994. Also lecture notes for ESSLLI'94, Copenhagen on
Inductive Definitions and Type Theory
Representing inductively defined sets by well-orderings in
Martin-Löf's type theory. Theoretical Computer
Science 176 (1997) pp 329-335.
A general formulation of simultaneous inductive-recursive definitions in
type theory , Journal
of Symbolic Logic, Volume 65, Number 2, June 2000, pp 525-549.
A finite axiomatization of inductive-recursive definitions
(with Anton Setzer ).
Pages 129 - 146 in Proceedings of TLCA 1999, LNCS 1581.
Indexed induction-recursion
(with Anton
Setzer ). Pages 93-113 in LNCS 2183, Proof Theory in Computer Science ·
International Seminar, PTCS 2001 Dagstuhl Castle, Germany, October
7-12, 2001.
Induction-recursion and initial algebras
(with Anton
Setzer ). Annals of Pure and
Applied Logic 124 (2003) 1-47.
Indexed induction-recursion
(with Anton
Setzer ). Journal of Logic and Algebraic Programming, volume 66,
Issue 1 , January 2006, Pages 1-49.
Some slides