Daniel Leivant
- {ANS82} A. Andreka. I. Nemeti and I Sain. A complete logic for reasoning about programs via non-standard model theory. Theoretical Computer Science 17 (1982) 193-212, 259-278.Google Scholar
Cross Ref
- {Apt81} Krzyszlof Apl. Ten years of Hoare's Logic: a survey -- part I; ACM Transactions on Programming languages and Systems 3 (1981) 431-483. Google ScholarDigital Library
- {Bro85} Stephen D. Brookes. On the axiomatic treatment of concurrency . Proceedings of the NSF-CERS Seminar on Concurrency. Spinger-Verlag. New York (1985).Google ScholarCross Ref
- {BT81} Jan A. Bergstra and John V. Tucker. Hoare's logic and Peano's Arithmic, Mathematisch Centrum REport IW 160/81 (1981) i+27.Google Scholar
- {deB80} Jaco de Bakker. Mathematical Theory of Program Correctness. Prentice-Hall. Englewood Cliffs (1980) xvii + 505. Google ScholarDigital Library
- {EFT84} H.D. Ebbinghaus. J. Flum and W. Thomas, Mathematical logis: Springer-Verlag. New York, (1984) ix + 216.Google Scholar
- {End70} Herbert B. Enderton. A Mathematical Introduction to logic: Academic Press. New York (1970) xiii + 295pp.Google Scholar
- {FLO83} Steven Fortune. Daniel Leivat. and Michael O'Donnell. "The expressiveness of simple and second order type structures," Journal of the ACM 30 (1983), pp. 151-185. Google ScholarDigital Library
- {FSS83} Harvey M. Friedman, Stephen G Simpson and Rick L. Smith, Countable algebras and set existence axioms, Annals of Pure and Applied Logic 25 (1983) 141-181.Google ScholarCross Ref
- {Gir72} Jean-Yves Girard. Interpretation fonctionelle et élimination des coupures dans l'arithmétique d'ordre superieur, Thèse de Doctorat d'Etat. 1972, Paris.Google Scholar
- {HA38} David Hilbert and Wilhelm Ackermann. Grundzuge der theoretischen Logik (Second Edition). Springer, Berlin (1938) viii+133. English translation: Principles of Mathematical Logic, Chelsea. New York (1950) xii + 172.Google Scholar
- {Har79} David Harel. First-Order Dyanmic Logic. Lecture Notes in Computer Science 68. Springer-Verlag, 1979.Google Scholar
- {Hen50} Leon Henkin. Completeness in the Theory of Types, Journal of Symbolic Logic 15 (1950), 81-91.Google ScholarCross Ref
- {KK67} Georg Kreisel and Jean-Louis Krivien, Elements de Logique Mathematique, Dunod. Paris (1967) viii+213.Google Scholar
- {Kle52} S. C. Kleene. Introductinn to Metamathematics, Noordhoff, Groningen (1952) x+550.Google Scholar
- {Lei83} Daniel Leivant. "Reasoning about functional programs and complexity classes associated with type disciplines". Twenty-fourth Annual Symposium on Foundations of Computer Science (1983) 460-469.Google Scholar
- {Lei84} Daniel Leivant. Typing and comvergence in the Lambda Calculus . manuscript (1984).Google Scholar
- {Lin69} Per Lindstrom. On extensions of elementary logic. Theoria 35 (1969) 1-11.Google ScholarCross Ref
- {MH82} Albert Meyer and Joseph Halpern. Axiomatic defition of programming languages: a theoretical assesment, Journal of the ACM 29 (1982) 555-576. Google ScholarDigital Library
- {MH82} Albert Meyer and John C. Mitchell. Termination assertions for recursive programs: complexity and axiomatic definability, Information and Control 56 (1983) 112-138.Google ScholarCross Ref
- {MPS84} David B. MacQueen, Gordin Plotkin and Ravi Sethi. "An ideal model for recursive polymorphic types," Conference Record of the Eleventh Annual ACM Symposium on Principles of Programming Languages (1984) 165-174. Google ScholarDigital Library
- {Nem82} I. Nemeti. Nonstandard dynamic logic; in: D. Kozen (ed.). Logics al Programs. Springer-Verlag (LNCS # 131). Beriin (1982) 311-348. Google ScholarDigital Library
- {OG76} Susan Owicki and David Gries. An axtomatic proof technique for parallel programs I. Acta Informatica 6 (1976) 319-340.Google ScholarDigital Library
- {Pra76} Vaughan Pratt, Semantical considerations on Floyd-Hoare logics , Proceedings of the Seventeenth IEEE Symposium on Foundntions of Computer Science (1976) 109-121.Google Scholar
- {Pra76} Vaughan Pratt. Applications of modal logic to programming, Studia Logica 39 (1980) 257-274.Google ScholarCross Ref
- {Pra71} Dag Prawitz. Ideas and results in Proof Theory. Proceedings of the Second Scandinavinn Logic Symposium (J.E. Fenstad, editor) North-Holland. Amsterdam (1971) 235-307.Google Scholar
- {Pra65} Dag Prawitz Natural Deduction. Almqvist and Wiksell, Uppsala, 1965.Google Scholar
- {Rey74} John C. Reynolds, Towards a theory of type structures, Programming Symposium (Colloque sur la Programmation, Paris). Springer (LNCS # 19). Berlin (1974) 408-425. Google ScholarDigital Library
- {Rog67} Hartley Rogers Jr., Theory of Recursive Functions and effective Computability, McGraw-Hill, New York (1967) ix + 482.Google Scholar
- {Rus20} Bertrand Russell. Introduction to Mathematical Philosophy, (Second Edition), London (1920).Google Scholar
- {Rus37} Bertrand Russell. Principles of Mathematics. (Second Edition). London (1937).Google Scholar
- {Tak75} Gaisi Takeuti. Proof Theory, North-Holland. Amsterdam (1975) vii+372.Google Scholar
- {Wan74} Hao Wang. From Mathematics to Philosophy. Roultege & Kegan Paul. London (1974) xiv+428.Google Scholar
- {Zuc80} Jeffery Zucker. Expressibility of pre- and post-conditions, in {deB80} 444-465.Google Scholar
Index Terms
- Logical and mathematical reasoning about imperative programs: preliminary report
Comments