Article

Free access

A Metalanguage for interactive proof in LCF

Authors:

C. WadsworthAuthors Info & Claims

POPL '78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

Pages 119 - 130

https://doi.org/10.1145/512760.512773

Published: 01 January 1978 Publication History

PDF eReader

References

[1]

Aiello, L., Aiello, M. & Wehyrauch, R., The semantics of PASCAL in LCF, AI Memo 221 Computer Science Dept., Stanford, 1974.

Digital Library

Google Scholar

[2]

Aubin, R., Mechanizing structural induction, Ph.D. thesis, University of Edinburgh, 1976.

Digital Library

Google Scholar

[3]

Boyer, R. S. & Moore, J. S., Proving theorems about LISP function, JACM 22,1 (Jan.1975), 129-144.

Digital Library

Google Scholar

[4]

Brown, F. M., A deductive System for Elementary Arithmetic. AISB Summer Conference, Edinburgh, 1976.

Google Scholar

[5]

de Bruijn, N. G., AUTOMATH, a language for mathematics, T.H.- Report 68-WSK-05, Dept. of Mathematics, Technological University, Eindhoven, Netherlands 1968.

Google Scholar

[6]

Burstall, R. M. & Popplestone, R., POP2 reference manual, in Machine Intelligence 2, eds. E. Dale & D. Michie, American Elsevier, New York, 1968, 205-246.

Google Scholar

[7]

Dahl, O.-J. et al, The SIMULA 67 Common base language, Norwegian Computing Centre, Oslo, 1968.

Digital Library

Google Scholar

[8]

Evans, A., PAL: a language designed for teaching programming linguistics, Proc. ACM 23rd Nat. Conf., 1968, Brandin Systems Press, Princeton, N. J., 395-403.

Digital Library

Google Scholar

[9]

Gordon, M., Milner, R. & Wadsworth, C. Edinburgh LCF, Department of Computer Science Internal Report CSR-11-77, University of Edinburgh, 1977.

Google Scholar

[10]

Guttag, J. V., The specification and application to programming of abstract data types, Ph.D. thesis, University of Toronto, 1975.

Digital Library

Google Scholar

[11]

Hayes, P. J., The language GOLUX. University of Essex, 1974.

Google Scholar

[12]

von Henke, F. N. & Luckham, D. C., A methodology for verifying programs, Proceedings of the International Conference on Reliable Software, Los Angeles, California 1975.

Digital Library

Google Scholar

[13]

Hewitt, C., PLANNER: a language for manipulating models and proving theorems in a robot, AI Memo 168, Project MAC, M.I.T., 1970.

Google Scholar

[14]

Hoare, C. A. R., An Axiomatic Basis for Computer Programming, CACM Vol.12, No.10, 1969.

Digital Library

Google Scholar

[15]

Landin, P. J., The next 700 programming languages, Comm. ACM 9,3 (March 1966), 157-166.

Digital Library

Google Scholar

[16]

Liskov, B. H. & Zilles, S., Programming with abstract data types, Proc. of a Symposium on Very High-Level Languages, SIGPLAN Notices 9,4 (April 1974), 50-59.

Digital Library

Google Scholar

[17]

Milner, R., Implementation and application of Scott's logic for computable functions, Proc. ACM Conf. on Proving Assertions about Programs, SIGPLAN Notices 7,1 (Jan.1972), 1-6.

Digital Library

Google Scholar

[18]

Milner, R., Logic for computable functions: description of a machine implementation, AI Memo 169, Computer Science Department, Stanford, 1972.

Digital Library

Google Scholar

[19]

Milner, R., Program semantics and mechanised proof, Proc. 2nd Advanced Course in Foundations of Computer Science, Mathematical Centre, Amsterdam, 1976.

Google Scholar

[20]

Milner, R., LCF: a methodology for performing rigorous proofs about programs, Proc. 1st IBM Symposium on Mathematical Foundations of Computer Science, Amagi, Japan, 1976.

Google Scholar

[21]

Milner, R., A Theory of Type Polymorphism in Programming, Department of Computer Science Internal Report CSR-9-77, University of Edinburgh, 1977.

Google Scholar

[22]

Milner, R., Morris, F. L. & Newey, M., A logic for computable functions with reflexive and polymorphic types, Proc. Conf. on Proving and Improving Programs, Arc-et-Senans, 1975.

Google Scholar

[23]

Milner, R. & Weyhrauch, R., Proving compiler correctness in a mechanised logic, in Machine Intelligence 7, ed. D. Michie, Edinburgh University Press, 1972.

Google Scholar

[24]

Newey, M., Formal semantics of LISP with applications to program correctness, Ph.D. thesis, Stanford, 1975.

Digital Library

Google Scholar

[25]

Reboh, R., Sacerdoti, E., A Preliminary QLISP Manual, Technical note 81, Artificial Intelligence Centre, SRI., Mento Park, California 1973.

Google Scholar

[26]

Reynolds, J. C., GEDANKEN: a simple typeless language based on the principle of completeness and the reference concept, Comm. ACM 13,5 (May 1970), 308-319.

Digital Library

Google Scholar

[27]

Robinson, J. A., A machine-oriented logic based on the resolution principle, JACM 12.1 (Jan. 1965) 23-41.

Digital Library

Google Scholar

[28]

Scott, D. S. & Strachey, C., Toward a Mathematical Semantics for Computer Languages, Proceedings of the Symposium on Computers and Automata, Microwave Research Institute Symposia Series, Vol.21, Polytechnic Institute of Brooklyn, 1972.

Google Scholar

[29]

Sussman, G., Winograd, T. & Charniak, E. Microplanner Reference Manual, AI Memo 203, Project MAC, M.I.T. 1970.

Digital Library

Google Scholar

[30]

Tennent, R. D., PASQUAL: a proposed generalisation of PASCAL, Tech. Report 75-32, Queens University, Kingston, Ontario, 1975.

Google Scholar

[31]

Topor, R. Interactive Program Verification using Virtual Programs, Ph.D. Thesis, Edinburgh, 1975.

Google Scholar

[32]

Waldinger, R. J. & Levitt, C., Reasoning about Programs, Artificial Intelligence, Vol.5 No.3.

Google Scholar

[33]

Weyhrauch, R. W. A User's Manual for FOL, Stanford Artificial Intelligence memo AIM 235.1, 1977.

Digital Library

Google Scholar

[34]

Weyhrauch, R. & Milner, R., Program semantics and correctness in a mechanised logic, Proc. USA - Japan Computer Conference, Tokyo, 1972.

Google Scholar

[35]

Wulf, R. A., London, R. L. & Shaw, M., Abstraction and verification in ALPHARD: introduction to language and methodology, Carnegie-Mellon University, 1976.

Crossref

Google Scholar

[36]

Zilles, S., Algebraic specification of data types, Computation Structures Group Memo 119, M.I.T., 1974.

Google Scholar

Cited By

View all

Kiselyov O(2024)Generating C: Heterogeneous metaprogramming system descriptionScience of Computer Programming10.1016/j.scico.2023.103015231(103015)Online publication date: Jan-2024
https://doi.org/10.1016/j.scico.2023.103015
Sewell TMyreen MTan YKumar RMihajlovic AAbrahamsson OOwens S(2023)Cakes That Bake Cakes: Dynamic Computation in CakeMLProceedings of the ACM on Programming Languages10.1145/35912667:PLDI(1121-1144)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591266
Arnaboldi LAspinall DKolb CRadomirović S(2023)Tactics for Account Access GraphsComputer Security – ESORICS 202310.1007/978-3-031-51479-1_23(452-470)Online publication date: 25-Sep-2023
https://dl.acm.org/doi/10.1007/978-3-031-51479-1_23
Show More Cited By

A Metalanguage for interactive proof in LCF
1. Mathematics of computing
  1. Continuous mathematics
    1. Calculus
2. Theory of computation

Recommendations

Formalizing a strong normalization proof for Moggi's computational metalanguage: a case study in Isabelle/HOL-nominal
LFMTP '09: Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice

Lindley and Stark have given an elegant proof of strong normalization for various lambda calculi whose type systems preclude a direct inductive definition of Girard-Tait style logical relations, such as the simply typed lambda calculus with sum types or ...
Soundness of Hoare's logic: an automated proof using LCF

This paper presents a natural deduction proof of Hoare's logic carried out by the Edinburgh LCF theorem prover. The emphasis is on the way Hoare's theory is presented to the LCF, which looks very much like an exposition of syntax and semantics to human ...
HOLCF = HOL + LCF

HOLCF is the definitional extension of Church's Higher-Order Logic with Scott's Logic for Computable Functions that has been implemented in the theorem prover Isabelle. This results in a flexible setup for reasoning about functional programs. HOLCF ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

POPL '78: Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

January 1978

264 pages

ISBN:9781450373487

DOI:10.1145/512760

Conference Chairs:
Alfred V. Aho
Bell Laboratories, Murray Hill, New Jersey
,
Stephen N. Zilles
IBM, San Jose, California
,
Program Chair:
Thomas G. Szymanski
Princeton University, Princeton, New Jersey

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1978

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

POPL '78 Paper Acceptance Rate 27 of 135 submissions, 20%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

55
Total Citations
View Citations
792
Total Downloads

Downloads (Last 12 months)114
Downloads (Last 6 weeks)12

Reflects downloads up to 22 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Kiselyov O(2024)Generating C: Heterogeneous metaprogramming system descriptionScience of Computer Programming10.1016/j.scico.2023.103015231(103015)Online publication date: Jan-2024
https://doi.org/10.1016/j.scico.2023.103015
Sewell TMyreen MTan YKumar RMihajlovic AAbrahamsson OOwens S(2023)Cakes That Bake Cakes: Dynamic Computation in CakeMLProceedings of the ACM on Programming Languages10.1145/35912667:PLDI(1121-1144)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591266
Arnaboldi LAspinall DKolb CRadomirović S(2023)Tactics for Account Access GraphsComputer Security – ESORICS 202310.1007/978-3-031-51479-1_23(452-470)Online publication date: 25-Sep-2023
https://dl.acm.org/doi/10.1007/978-3-031-51479-1_23
MacQueen DHarper RReppy J(2020)The history of Standard MLProceedings of the ACM on Programming Languages10.1145/33863364:HOPL(1-100)Online publication date: 12-Jun-2020
https://dl.acm.org/doi/10.1145/3386336
Wenzel M(2019)Interaction with Formal Mathematical Documents in Isabelle/PIDEIntelligent Computer Mathematics10.1007/978-3-030-23250-4_1(1-15)Online publication date: 3-Jul-2019
https://doi.org/10.1007/978-3-030-23250-4_1
Omar CVoysey IHilton MAldrich JHammer M(2017)Hazelnut: a bidirectionally typed structure editor calculusACM SIGPLAN Notices10.1145/3093333.300990052:1(86-99)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009900
Omar CVoysey IHilton MAldrich JHammer MCastagna GGordon A(2017)Hazelnut: a bidirectionally typed structure editor calculusProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009900(86-99)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009900
Naujokat SNeubauer JMargaria TSteffen B(2016)Meta-Level Reuse for Mastering Domain SpecializationLeveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications10.1007/978-3-319-47169-3_16(218-237)Online publication date: 5-Oct-2016
https://doi.org/10.1007/978-3-319-47169-3_16
Kirchner H(2015)Rewriting Strategies and Strategic Rewrite ProgramsLogic, Rewriting, and Concurrency10.1007/978-3-319-23165-5_18(380-403)Online publication date: 27-Aug-2015
https://doi.org/10.1007/978-3-319-23165-5_18
Solodkyy YDos Reis GStroustrup B(2013)Open pattern matching for C++ACM SIGPLAN Notices10.1145/2637365.251722249:3(33-42)Online publication date: 27-Oct-2013
https://dl.acm.org/doi/10.1145/2637365.2517222
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Recommendations

Formalizing a strong normalization proof for Moggi's computational metalanguage: a case study in Isabelle/HOL-nominal

Soundness of Hoare's logic: an automated proof using LCF

HOLCF = HOL + LCF