A Home Page on Higher-Order Specifications.

Latest update 28th January 1997.

Please send comments to: <karlm@nada.kth.se>

Introduction.

It will include an on-line bibliography.

Here is a link to information on the forthcoming conference Higher-Order Algebra, Logic and Term Rewriting: HOA '97,

Here is a link to an electronic discussion forum on higher-order specifications organised within the algebraic specification project CoFI

This page is under construction, and is going to take some time to complete!

On-Line Bibliography.

Relevant Survey Articles.

D. Leivant, Higher-order logic, in: D. Gabbay, C.J. Hogger and J.A. Robinson (eds), Handbook of Logic in Artificial Intelligence and Logic Programming, Vol 5, Oxford University Press, 1993.

K. Meinke, A Survey of Higher-Order Algebra, Technical Report, UUDM 1995:39, ISSN 1101-3591, Department of Mathematics, University of Uppsala, 1995.

J. Van Benthem and K. Doets, Higher-order logic, 275-330 in: D. Gabbay and F. Guenthner (eds), Handbook of Philosophical Logic, Vol 1, D. Reidel, Dordrecht, 1983.

Relevant Conference Proceedings.

J. Heering, K. Meinke, B. Möller, T. Nipkow (eds), HOA '95: Proc. First Int. Workshop on Higher-Order Algebra, Logic and Term Rewriting, Lecture Notes in Computer Science 1074, Springer Verlag, Berlin, 1996.

PhD and Habilitation Theses.

B.M. Hearn, The Design and Implementation of Typed Languages for Algebraic Specification, PhD Thesis, Dept. of Computer Science, University of Wales, Swansea, 1995.

B. Möller, Higher-order algebraic specifications, Fakultät fuer Mathematik und Informatik, Technische Universität Muenchen, Habilitationsschrift, 1987.

K. Parsaye-Ghomi, Higher-order abstract data types, Department of Computer Science, University of California at Los Angeles, PhD thesis, (1981).

L.J. Steggles, Extensions of Higher-Order Algebra: Fundamental Theory and Case Studies, PhD Thesis, Dept. of Computer Science, University of Wales, Swansea, 1995.

Research Papers.

E. Astesiano and M. Cerioli. Partial Higher-Order Specifications (Extended version), Fundamenta Informaticae, 16(2):101--126, 1992.

M. Broy, Equational specification of partial higher-order algebras, in: M. Broy (ed) Logic of programming and calculi of discrete design, (Springer Verlag, Berlin, 1987).

A. Church, A formulation of the simple theory of types, Journal of Symbolic Logic 5 (1940), 56-68.

L. Chwistek, Antynomje logikiformalnej. Przegl.fil. vol 24, 164-171, english translation in Storrs McCall (ed), Oxford, 1967.

L. Chwistek, Uber die Antinomien der Prinzipen der Mathematik, Mathematik Zeitschrift 14, (1922), 236-243.

J.P. Cleave, Local properties of systems, J. London Math. Soc. 44 (1969) 121-30.

R.O. Gandy, The simple theory of types, in: R. Gandy and M. Hyland (eds) Logic Colloquium 76, (North Holland, Amsterdam, 1977).

M. Gordon, Why higher-order logic is a good formalism for specifying and verifying hardware, in: G. Milne and P.A. Subrahmanyam, (eds) Formal aspects of VLSI design, (North Holland, Amsterdam, 1986).

J.A. Goguen, Higher-order functions considered unnecessary for higher-order programming, 309-352 in D.A. Turner (ed), Research Topics in Functional Programming, Addison Wesley, 1990.

F.K. Hanna and N. Daeche, Specification and verification using higher-order logic, in: C.J. Koomen and T. Moto-oka (eds), Proceedings of the 7th International Conference on Computer Hardware Description Languages and their Applications, 418-419, North Holland, Amsterdam, 1985.

W.S. Hatcher, The logical foundations of mathematics, (Pergamon Press, Oxford, 1982).

L. Henkin, Completeness in the theory of types, J. Symbolic Logic 2 (1950) 81--91 .

L. Henkin, A theory of propositional types, Fund. Math., 52 (1963), 323-344.

M. Hofmann and D. Sannella. On behavioural abstraction and behavioural satisfaction in higher-order logic. Theoretical Computer Science 167:3-45 (1996).

G. Kreisel and J.L. Krivine, Elements of mathematical logic: model theory, (North Holland, Amsterdam, 1967).

T.S.E. Maibaum and C.J. Lucena, Higher-order data types, International Journal of Computer and Information Sciences 9, (1980) 31--53.

K. Meinke, Equational specification of abstract types and combinators, pp. 257-271 in: E. Börger et al (eds), Proc. Computer Science Logic '91, Lecture Notes in Computer Science 626, Springer Verlag, Berlin, 1992.

K. Meinke, Algebraic semantics of rewriting terms and types, pp. 1-20 in: J.L. Remy and M. Rusinowitch (eds), Proc. Third International Workshop on Conditional Term Rewriting Systems, Lecture Notes in Computer Science 656, Springer Verlag, Berlin, 1993.

K. Meinke and L.J. Steggles, Specification and verification in higher-order algebra: a case study of convolution, pp. 189-222 in: J. Heering et al (eds), HOA '93, an International Workshop on Higher-Order Algebra, Logic and Term Rewriting, Lecture Notes in Computer Science 816, Springer Verlag, Berlin, 1994.

B.M. Hearn and K. Meinke, ATLAS: A Typed Language for Algebraic Specifications, pp. 146-168 in: J. Heering et al (eds), HOA '93, an International Workshop on Higher-Order Algebra, Logic and Term Rewriting, Lecture Notes in Computer Science 816, Springer Verlag, Berlin, 1994.

K. Meinke, Higher-order equational logic for specification, simulation and testing, pp. 124-143 in: J. Heering et al (eds), HOA '95, an International Workshop on Higher-Order Algebra, Logic and Term Rewriting, Lecture Notes in Computer Science 1074, Springer Verlag, Berlin, 1996.

K. Meinke, Universal algebra in higher types, Theoretical Computer Science, 100, (1992), 385-417.

K. Meinke, Subdirect representation of higher-order algebras, 135-146 in: K. Meinke and J.V. Tucker (eds), Many-Sorted Logic and its Applications, John Wiley, Chichester, 1993.

K. Meinke, A recursive second-order initial algebra specification of primitive recursion, Acta Informatica, 31, (1994), 329-340.

P. Kosiuczenko and K. Meinke, On the power of higher-order algebraic specification methods, Information and Computation, 124, (1995), 85-101.

K. Meinke, Topological methods for algebraic specification, Theoretical Computer Science, 166, (1996), 263-290.

K. Meinke, A completeness theorem for the expressiveness of higher-order algebraic specifications, to appear in Journal of Computer and Systems Sciences, 1997.

K. Meinke and L.J. Steggles, Correctness of Dataflow and Systolic Algorithms: Case Studies in Higher-Order Algebra, unpublished report, 1997.

K. Meinke, Proof Theory of Higher-Order Equations: Conservativity, Normal Forms and Term Rewriting, unpublished report, 1997.

D.A. Miller and G. Nadathur, Higher-order logic programming, Departmental Report MS-CIS-86-17, University of Pennsylvania, Department of Computer and Information Science, 1986.

B. Möller, Algebraic specifications with higher-order operators, in: L.G.L.T. Meertens (ed) Program specification and transformation, (North Holland, Amsterdam, 1987a).

B. Möller, A. Tarlecki and M. Wirsing, Algebraic specifications of reachable higher-order algebras, in: D. Sannella and A. Tarlecki (eds), Recent Trends in Data Type Specification, Lecture Notes in Computer Science 332,(Springer Verlag, Berlin, 1988) 154-169.

G. Nadathur and D. Miller, Higher-Order Horn Clauses, Journal of the Association for Computing Machinery, 37, (1990), 777-814.

S. Orey, Model Theory for the Higher Order Predicate Calculus, Trans. Amer. Math Soc. 92, (1959), 72-84.

A. Poigne, On specifications, theories and models with higher types, Information and Control 68, (1986) 1-46.

Up to Karl Meinke's home page.