Abstract
In his lecture at the congress, the first author gave a survey on some recent results relevant for computability theory in the context of partial continuous functionals (cf. (Scott, 1982; Ershov, 1977; Stoltenberg-Hansen et al., 1994)):
-
An abstract definition of totality due to Berger (cf. (Berger, 1990; Berger, 1993) and (Stoltenberg-Hansen et al., 1994, Ch. 8.3)), and applications concerning density and effective density theorems.
-
Bounded fixed points: one can have the flexibility of fixed point definitions and termination at the same time (cf. (Schwichtenberg and Wainer, 1995)).
-
A notion of strict functionals as a tool to prove termination of higher order rewrite systems (cf. (van de Pol and Schwichtenberg, 1995)) .
The first author is partially supported by the working group Nada (New Hardware Design Methods) of the Ec, and the second author is partially supported by a grant from the German Federal Ministry of Education, Science, Research, and Technology under contract number 01IS519A (project KorSys).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ulrich Berger. Totale Objekte und Mengen in der Bereichstheorie. PhD thesis, Mathematisches Institut der Universität München, 1990.
Ulrich Berger. Total sets and objects in domain theory. Annals of Pure and Applied Logic, 60:91–117, 1993.
Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In Rao Vemuri, editor, Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pages 203–211. IEEE Computer Society Press, Los Alamitos, 1991.
Luc Claesen, editor. Formal VLSI Specification and Synthesis VLSI Design Methods I and II. IFIP, sponsored by IMEC, North—Holland, Amsterdam, 1990.
Yuri L. Ershov. Model C of partial continuous functionals. In R. Gandy and M. Hyland, editors, Logic Colloquium 1976, pages 455–467. North—Holland, Amsterdam, 1977.
Mike Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G.J. Milne and P.A. Subrahmanyam, editors, Formal Aspects of VLSI Design, pages 153–177. Elsevier, Amsterdam, 1986.
Thomas Kropf. Benchmark-circuits for hardware-verification. In R. Kumar and T. Kropf, editors, Theorem Provers in Circuit Design (TPCD ’94), volume 901 of Lecture Notes in Computer Science, pages 1–12. Springer Verlag, Berlin, Heidelberg, New York. 1995.
Jaco van de Pol and Helmut Schwichtenberg. Strict functionals for termination proofs. In M. Dezani-Ciancaglini and G. Plotkin, editors, Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, pages 350–364. Springer Verlag, Berlin, Heidelberg, New York, 1995.
Helmut Schwichtenberg. Proofs as programs. In P. Aczel, H. Simmons, and S.S. Wainer, editors, Proof Theory. A selection of papers from the Leeds Proof Theory Programme 1990, pages 81–113. Cambridge University Press, 1993.
Helmut Schwichtenberg and Stanley S. Wainer. Ordinal bounds for programs. In P. Clote and J. Remmel, editors, Feasible Mathematics II, pages 387–406. Birkhäuser, Boston, 1995.
Dana Scott. Domains for denotational semantics. In E. Nielsen and E.M. Schmidt, editors, Automata, Languages and Programming, volume 140 of Lecture Notes in Computer Science, pages 577–613. Springer Verlag, Berlin, Heidelberg, New York, 1982. A corrected and expanded version of a paper prepared for ICALP’82, Aarhus. Denmark.
Viggo Stoltenberg-Hansen, Edward Griffor, and Ingrid Lindström. Mathematical Theory of Domains. Cambridge tracts in Theoretical Computer Science. Cambridge University Press, 1994.
Karl Stroetmann. SEDUCT — a proof compiler for first order logic. In M. Broy and S. Jähnichen, editors, KORSO: Methods, Languages and Tools for the Construction of Correct Software. Final Report, volume 1009 of Lecture Notes in Computer Science, pages 299–316. Springer Verlag, Berlin, Heidelberg, New York, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 Springer Science+Business Media Dordrecht
About this chapter
Cite this chapter
Schwichtenberg, H., Stroetmann, K. (1997). From Higher Order Terms To Circuits. In: Dalla Chiara, M.L., Doets, K., Mundici, D., van Benthem, J. (eds) Logic and Scientific Methods. Synthese Library, vol 259. Springer, Dordrecht. https://doi.org/10.1007/978-94-017-0487-8_11
Download citation
DOI: https://doi.org/10.1007/978-94-017-0487-8_11
Publisher Name: Springer, Dordrecht
Print ISBN: 978-90-481-4786-1
Online ISBN: 978-94-017-0487-8
eBook Packages: Springer Book Archive