A stratified semantics of general references embeddable in higher-order logic
Proceedings - Symposium on Logic in Computer Science - Trang 75-86
Tóm tắt
We demonstrate a semantic model of general references - that is, mutable memory cells that may contain values of any (statically-checked) closed type, including other references. Our model is in terms of execution sequences on a von Neumann machine; thus, it can be used in a Proof-Carrying Code system where the skeptical consumer checks even the proofs of the typing rules. The model allows us to prove a frame-axiom introduction rule that allows locality of specification and reasoning, even in the event of updates to aliased locations. Our proof is machine-checked in the Twelf metalogic.
Từ khóa
#Logic #Object oriented modeling #Safety #Data structures #Java #Arithmetic #Computer languages #Computer scienceTài liệu tham khảo
10.1145/263699.263712
10.1016/0304-3975(91)90033-X
10.1145/319301.319345
levy, 2001, Call-by-Push-Value
michael, 2000, Machine instruction syntax and semantics in higher-order logic, Proc 17th Int l Conf Automated Deduction, 10.1007/10721959_2
huth, 2000, Logic in Computer Science Modelling and Reasoning about Systems
10.1145/360204.375719
hintikka, 1975, Impossible possible worlds vindicated, Journal of Philosophical Logic, 4, 475, 10.1007/BF00558761
hudak, 1992, Report on the programming language Haskell, a non-strict, purely functional language, SIGPlan Notices, 27, 10.1145/130697.130699
oles, 1982, A Category-Theoretic Approach to the Semantics of Programming Languages
10.2307/421090
10.1007/978-1-4757-3851-3_1
park, 1969, Fixpoint induction and proofs of program properties, Machine Intelligence, 5, 59
peregrin, 1993, Possible worlds: A critical analysis, The Prague Bulletin of Mathematical Linguistics, 59 60, 9
pfenning, 1999, System description: Twelf - A meta-logical framework for deductive systems, 11th Int Conf on Automated Deduction
pitts, 1993, Observable properties of higher order functions that dynamically create local names, or: What's new?, Mathematical Foundations of Computer Science, 711, 122
reynolds, 1981, The essence of Algol, Algorithmic Languages, 345
reynolds, 2000, Intuitionistic reasoning about shared mutable data structure, Millennial Perspectives in Computer Science, 303
kripke, 1963, Semantical considerations on modal logic, Proceedings of a Colloquium Modal and Many Valued Logics, 16, 83
ahmed, 2002, A stratified semantics of general references embeddable in higher-order logic (extended version)
aczel, 1988, Non-well-founded Sets
10.1145/138027.138060
10.1109/LICS.1998.705669
stark, 1994, Names and Higher-order Functions
burstall, 1972, Some techniques for proving correctness of programs which alter data structures, Machine Intelligence, 7, 23
barwise, 1996, Vicious Circles On the Mathematics of Non-wellfounded Phenomena
10.1016/0890-5401(90)90018-D
appel, 2000, An indexed model of recursive types for foundational proof-carrying code
swadi, 2002, Foundational semantics for TAL syntactic rules via typed machine language
10.1145/325694.325727
10.1016/0020-0190(94)90120-1
fiore, 1996, Domains and denotational semantics History accomplishments and open problems, 30