Programming Language Semantics Research at Kansas State University

This writeup is terribly out of date! I am leaving the existing materials in place because they give a nice historical picture as to how things got started. A more up-to-date view can be found here.

*Dave Schmidt, 2 December 98*.

An early theme was static analysis of denotational semantics definitions to deduce when a definition's store and environment arguments could be implemented in the conventional way, that is, as global run-time and compile-time data structures [Schmidt85, Schmidt88]. Such "single-threading" techniques form the heart of compiler production from denotational semantics definitions.

Compiler production also benefits from a proper understanding of the relation between compile-time and run-time processing. Partial evaluation provides a good basis for identifying a language's compile-time actions and staging them into a compiler [ConselDanvy93, Malmkjaer93]. Partial evaluation works well with continuation-passing style (CPS), and research in the group established the connections between various forms of the CPS transformations [DanvyHatcliff93, Hatcliff94, HatcliffDanvy94].

Compiler construction based upon action semantics definitions was another area of activity within the department. In particular, action semantics definitions are written at a level of modularity that allows simpler analysis of binding times, types, and single-threading than one must do for conventional denotational semantics definitions [EvenSchmidt90, DohSchmidt93].

Another compilation-related project was a study of static analysis techniques that admitted implementation of higher-order functional languages with a classic, stack-based environment [BanerjeeSchmidt94, Banerjee95]. Research on properties of algebraic semantics also fits into the above [Zamfir-Bleyberg87].

The group's research in foundational areas has taken several paths.

One direction of work was concerned with definability of elements in models of typed lambda calculi. An algorithm was developed that decides whether there exists a definable element of a finite model of an applied typed lambda calculus that passes certain tests, in the special case when all the constants and test arguments are of order at most one [Stoughton94]. When there is such an element, the algorithm outputs a term that passes the tests; otherwise, the algorithm outputs a logical relation that demonstrates the nonexistence of such an element. lambda, the ANSI C implementation of this algorithm, is available.

Another line of work focussed upon models for higher-order lambda calculus with subtyping. Based on concepts from functor categories and category-sorted algebra, a model was developed that supports subtyping with coercion functions that are non-embeddings [Fiech93, Fiech94, FiechHuth94, FiechSchmidt96]. Such a structure is important to modelling realistic polymorphic programming languages and lends insight to existing models.

[BanerjeeSchmidt93] A. Banerjee and D.A. Schmidt. A categorical interpretation of Landin's correspondence principle. Proceedings 9th Conf. Mathematical Foundations of Programming Semantics, S. Brookes, et al., eds., Springer LNCS 802, 1993, pp. 587-602.

[BanerjeeSchmidt94] A. Banerjee and D.A. Schmidt. Stackability in the call-by-value typed lambda calculus. Science of Computer Programming, to appear. (Preliminary version appears in Proc. Symposium on Static Analysis, Springer LNCS 864, pp. 131-146.)

[ConselDanvy93] C. Consel and O. Danvy. Tutorial notes on partial evaluation. Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages, Charleston, South Carolina, January 1993, ACM Press, 493-501.

[DanvyHatcliff93] O. Danvy and J. Hatcliff. CPS transformation after strictness analysis. ACM Letters on Programming Languages and Systems 1(3):195-212, 1993.

[DohSchmidt93] K.-G. Doh and D.A. Schmidt. Action semantics-directed prototyping. Computer Languages 19-4 (1993) 213-233.

[EvenSchmidt90] S. Even and D.A. Schmidt. Category sorted algebra-based action semantics. Theoretical Computer Science 77-1,2 (1990) 73-96.

[Fiech93] A. Fiech. A Denotational Model for Polymorphic Lambda Calculus with Subtyping. Ph.D. dissertation, Kansas State University, 1993.

[Fiech94] A. Fiech. Colimits in the category CPO. Mathematical Structures in Computer Science, in press.

[FiechHuth94] A. Fiech and M. Huth. Algebraic domains of natural transformations. Theoretical Computer Science, in press.

[FiechSchmidt96] A. Fiech and D.A. Schmidt. Polymorphic Lambda Calculus and Subtyping. Submitted for journal publication.

[Hatcliff94] John Hatcliff. The Structure of Continuation-Passing Styles. Ph.D. dissertation, Kansas State University, 1994.

[HatcliffDanvy94] J. Hatcliff and O. Danvy. A generic account of continuation-passing styles. In Hans-J. Boehm, editor, Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, Portland, Oregon, January 1994, ACM Press, 448-471.

[Howard92] B. Howard. Fixed Points and Extensionality in Typed Functional Programming Languages. Report STAN-CS-92-1445, Computer Science Dept., Stanford Univ., 1992.

[Howard94] B. Howard. Another iteration on Darlington's ``A Synthesis of Several Sorting Algorithms''. Report 94-8, Computing Info. Sci., Kansas State Univ., 1994.

[Howard95] Brian Howard. Fixpoint Computations and Coiteration. Report 95-1, Computer Science Department, Kansas State University, Manhattan, KS, 1995

[Howard96] Brian Howard. Fixpoint Computations and Coiteration. In 1996 ACM SIGPLAN International Conference on Functional Programming, Philadelphia, May 24-26, 1996.

[JungStoughton93] A. Jung and A. Stoughton. Studying the fully abstract model of PCF within its continuous function model. International Conference on Typed Lambda Calculi and Applications, LNCS 664, Springer-Verlag, 1993, 230-244.

[Komagata95] Y. Komagata and D. Schmidt. An Implementation of Intuitionistic Type Theory and Realizability Theory. Report 95-4,Computing Info. Sci., Kansas State Univ., 1995.

[Kotov95] Sergey Kotov. On logical relations for properties at higher types. Report 95-3, Computer Science Department, Kansas State University, Manhattan, KS, 1995.

[Malmkjaer93] K. Malmkjaer. Abstract Interpretation and Partial Evaluation. Ph.D. dissertation, Kansas State University, 1993.

[MizunoSchmidt92] M. Mizuno and D.A. Schmidt. A security flow control algorithm and its denotational semantics correctness proof. Formal Aspects of Computing 4 (1992) 727-754.

[Schmidt85] D.A. Schmidt. Detecting global variables in denotational specifications. ACM Transactions on Programming Languages and Systems 7-2 (1985) 299-310.

[Schmidt86] D.A. Schmidt. Denotational Semantics: A Methodology for Language Development. Wm. C. Brown, Dubuque, IA, 1986.

[Schmidt88] D.A. Schmidt. Detecting stack-based environments in denotational definitions. Science of Computer Programming 11-2 (1988) 107-133.

[Schmidt94] D.A. Schmidt. The Structure of Typed Programming Languages. MIT Press, Cambridge, Massachusetts, 367 pages, 1994.

[Schmidt95a] D.A. Schmidt. Programming Language Semantics. In CRC Handbook of Computer Science, Allen Tucker, ed., CRC Press, Boca Raton, FL, in press.

[Schmidt95b] D.A. Schmidt. Natural-semantics-based abstract interpretation. Proc. 1995 Static Analysis Symposium, Glasgow, A. Mycroft, ed., Springer LNCS, in press.

[Schmidt96] D.A. Schmidt. Abstract interpretation of small-step semantics . Proc. 1996 LOMPAS Workshop on Multiple-Agent Languages, M. Dam and F.Orava, eds. , Report 96-05, Swedish Inst. Computer Science, Stockholm.

[Stoughton88] A. Stoughton. Fully Abstract Models of Programming Languages. Research Notes in Theoretical Computer Science, Pitman/Wiley, 123 pages, 1988.

[Stoughton90] A. Stoughton. Equationally fully abstract models of PCF. Fifth International Conference on the Mathematical Foundations of Programming Semantics, LNCS 442, Springer-Verlag, 1990, 271-283.

[Stoughton91] A. Stoughton. Parallel PCF has a unique extensional model. Sixth Annual IEEE Symposium on Logic in Computer Science, 1991, 146-151.

[Stoughton94] A. Stoughton. Mechanizing Logical Relations. Ninth International Conference on the Mathematical Foundations of Programming Semantics, LNCS, Springer-Verlag, 1994, in press.

[Zamfir-Bleyberg87] M. Zamfir-Bleyberg. Initial algebra semantics and concurrency. Proceedings Third Workshop on Mathematical Foundations of Programming Semantics, LNCS 298, Springer-Verlag, 1987, 528-549.

Dave Schmidt (schmidt@cis.ksu.edu)