• Articles •     Next Articles

A Type-Theoretic Approach to Program Development

Li Wei;   

  1. Beijing University of Aeronautics and Astronautics;
  • Online:1990-05-10 Published:1990-05-10

A paradigm of program development using type theories is given after analyzing some typical exam- ples.In order to carry this approach forward,a language ALT is designed.It is a linguistic description of a generalized higher order typed lambda calculus with Π,∑ types and Π,∑ kinds (supertypes). Four examples are given to show how ALT can be used to implement many concepts of software engi- neering and artificial intelligence.They are intuitionistic logic,Peano arithmetic,approximate reasoning and program tr…

Key words: design for yield; critical area; gridless routing; integrated circuit layout;

[1] A.Avron, F.A.Honsell and I.A.Mason, Using Typed Lambda Calculus to Implement Formal Systems on a Machine, Technical Report of LFCS, ECS-LFCS-87-31,University of Edinburgh. July 1987.

[2] M.Broy. Algebraic Methods for Program Construction:The Project CIP. Program Transformation and Programming Environments. NATO ASI Series. 1984.

[3] L.Cardelli. Polymorphic \-Calculus with Type:Type. Technical Report No.10,System Research Center. May 1986.

[4] L.Cardelli. Structural subtyping and the notion of poor type, Proc. POPL 1988.

[5] L.Cardelli. A Quest Preview. A Draft of Technical Report. System Research Center. January, 1988.

[6] Conquand and G. Huet, A High-Order Proof System for Mechanizing Mathematics. EUROCAL' 85,SpringerVerlag. 1985.
[1] Qiang Zhou, Yi-Ci Cai, Duo Li, and Xian-Long Hong. A Yield-Driven Gridless Router [J]. , 2007, 22(5): 653-660 .
Full text



No Suggested Reading articles found!

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved