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.

Overview

Semantics research at Kansas State University has been active since 1984. The semantics group currently consists of five faculty, three Ph.D. students, and several M.S. students. The group has maintained ties to like-minded groups in Scotland (Glasgow and Edinburgh), Denmark (Copenhagen and Aarhus), and France (Rennes), and exchanges of students and visitors between groups has been frequent. These connections have been absorbed recently into the "Atlantique" consortium, which sponsors regularly scheduled meetings. The group has also been active in the Mathematical Foundations of Programming Semantics, Partial Evaluation and Semantics-Based Manipulation, and Static Analysis Symposium meetings. The group is funded (from time to time) by the National Science Foundation, the Office of Naval Research, and DARPA.

Past Research

Over the past ten years, the group has concentrated upon putting semantics "to work" in techniques and tools for language design and implementation.

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.

Current Research

Here is a sampling of the group's current research projects:

Abstract interpretation of operational semantics

Cousot-Cousot-style abstract interpretation was developed originally for flowchart languages and adapted to denotational semantics; the latter formulation displayed a tension in its attempted reconciliation of intensional property extraction from an extensional definition format. To relieve this tension, studies of abstract interpretation of natural (big-step) and structural operational (small-step) semantics are being undertaken [Schmidt95b, Schmidt96]. Application of coinductive definition and proof techniques lead to simple, intuitive explanations of fundamental abstract interpretation concepts such as concrete and abstract collecting semantics and motivate new concepts such as ``intensional logical relations.''

Full Abstraction and the Applied Typed Lambda Calculus PCF

Research continues on full abstraction and on models for the applied typed-lambda-calculus PCF [Stoughton88]. Topics of interest include: (i) the relationship between models of PCF over the booleans and models of ordinary PCF, (ii) the category of equationally fully abstract models of PCF [Stoughton90], and (iii) the relationship of PCF's continuous function model to its inequationally fully abstract model [JungStoughton93].

Applications of type theory

As an outgrowth of the work of Howard [Howard92], the group is investigating applications of type theory to algorithm design and programming in-the-large. This includes a type-theoretic characterization of the taxomony of sorting algorithms [Howard94], the languages with inductive and coinductive type definition mechanisms [Howard95,Howard96], design of linking languages for a modules language based on type theory, adaptaption of realizability theory for practical programming, and implementation of tools based on these ideas [Komagata95].

References

[Banerjee95] Anindya Banerjee. The semantics and implementation of bindings in higher-order programming languages. Ph.D. dissertation, Kansas State University, 1995.

[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)