Commit | Line | Data |
---|---|---|
42d6e430 BJ |
1 | %A A. V. Aho |
2 | %A C. Beeri | |
3 | %A J. D. Ullman | |
4 | %T The Theory of Joins in Relational Databases | |
5 | %J Proc. 18th IEEE Symp. on Foundations of Computer Science | |
6 | %D 1977 | |
7 | ||
8 | %A A. V. Aho | |
9 | %A Y. Sagiv | |
10 | %A J. D. Ullman | |
11 | %T Equivalence of Relational Expressions | |
12 | %O unpublished | |
13 | %D 1977 | |
14 | ||
15 | %A W. W. Armstrong | |
16 | %T Dependency Structures of Data Base Relationships | |
17 | %J Proc. IFIP 74 | |
18 | %I North Holland | |
19 | %D 1974 | |
20 | %P 580-583 | |
21 | ||
22 | %A P. A. Bernstein | |
23 | %A C. Beeri | |
24 | %T An Algorithmic Approach to Normalization of Relational Database Schemes | |
25 | %R TR CSRG-7B | |
26 | %I Computer Science Research Group, University of Toronto | |
27 | %D September 1976 | |
28 | ||
29 | %A C. Beeri | |
30 | %A R. Fagin | |
31 | %A J. H. Howard | |
32 | %T A Complete Axiomatization for Functional and Multivalued Dependencies | |
33 | %R RJ1977 | |
34 | %I IBM, San Jose, California | |
35 | %D 1977 | |
36 | ||
37 | %A A. K. Chandra | |
38 | %A P. M. Merlin | |
39 | %T Optimal Implementation of Conjunctive Queries in Relational Data Bases | |
40 | %J Proc. 9th ACM Symp. on Theory of Computing | |
41 | %D 1976 | |
42 | %P 77-90 | |
43 | ||
44 | %A E. F. Codd | |
45 | %T A Relational Model for Large Shared Data Bases | |
46 | %J Comm. Assoc. Comp. Mach. | |
47 | %K acm cacm | |
48 | %V 13 | |
49 | %N 6 | |
50 | %D June 1970 | |
51 | %P 377-387 | |
52 | ||
53 | %A E. F. Codd | |
54 | %T Further Normalization of the Data Base Relational Model | |
55 | %B Data Base Systems | |
56 | %E R. Rustin | |
57 | %I Prentice Hall | |
58 | %C Englewood Cliffs, N. J | |
59 | %D 1972 | |
60 | %P 33-64 | |
61 | ||
62 | %A E. F. Codd | |
63 | %T Relational Completeness of Data Base Sublanguages | |
64 | %B Data Base Systems | |
65 | %E R. Rustin | |
66 | %I Prentice-Hall | |
67 | %C Englewood Cliffs, N. J | |
68 | %D May 1971 | |
69 | %P 65-98 | |
70 | ||
71 | %A S. A. Cook | |
72 | %T The Complexity of Theorem Proving Procedures | |
73 | %J Proc. 3rd ACM Symp. on Theory of Computing | |
74 | %D May 1971 | |
75 | %P 151-158 | |
76 | ||
77 | %A C. J. Date | |
78 | %T An Introduction to Database Systems | |
79 | %I Addison-Wesley | |
80 | %C Reading, Mass | |
81 | %D 1975 | |
82 | ||
83 | %A C. Delobel | |
84 | %T Contributions Theoretiques a la Conception d'un Systeme d'informations | |
85 | %O Ph. D. thesis, Univ. of Grenoble, Oct | |
86 | %D 1973 | |
87 | ||
88 | %A R. Fagin | |
89 | %T Multivalued Dependencies and a New Normal Form for Relational Databases | |
90 | %J ACM Trans. Data Base Systems | |
91 | %V 2 | |
92 | %N 3 | |
93 | %D September 1977 | |
94 | %P 262-278 | |
95 | ||
96 | %A P. A. V. Hall | |
97 | %T Optimization of a Single Relational Expression in a Relational | |
98 | Database System | |
99 | %J IBM J. Research and Development | |
100 | %D May 1976 | |
101 | %P 244-257 | |
102 | ||
103 | %A R. M. Karp | |
104 | %T Reducibility Among Combinatorial Problems | |
105 | %B Complexity of Computer Computations | |
106 | %E R. E. Miller and J. W. Thatcher | |
107 | %I Plenum Press | |
108 | %C New York | |
109 | %D 1972 | |
110 | %P 85-104 | |
111 | ||
112 | %A C. L. Lucchesi | |
113 | %A S. L. Osborn | |
114 | %T Candidate Keys for Relations | |
115 | %J J. Comp. Sys. Sci. | |
116 | %O (To appear; available from Department of Computer Science, University of Waterloo). | |
117 | %D 1976 | |
118 | ||
119 | %A J. Minker | |
120 | %T Performing Inferences over Relational Databases | |
121 | %R TR363, Department of Computer Science | |
122 | %I University of Maryland | |
123 | %D March 1975 | |
124 | ||
125 | %A R. M. Pecherer | |
126 | %T Efficient Evaluation of Expressions in a Relational Algebra | |
127 | %J Proc. ACM Pacific Conf. | |
128 | %D April 1975 | |
129 | %P 44-49 | |
130 | ||
131 | %A F. P. Palermo | |
132 | %T A Database Search Problem | |
133 | %B Information Systems COINS IV | |
134 | %E J. T. Tou | |
135 | %I Plenum Press | |
136 | %C New York | |
137 | %D 1974 | |
138 | ||
139 | %A J. Rissanen | |
140 | %T Independent Components of Relations | |
141 | %R RJ1899, IBM, San Jose, California | |
142 | %D 1977 | |
143 | ||
144 | %A Y. Sagiv | |
145 | %A M. Yannakakis | |
146 | %T unpublished | |
147 | ||
148 | %A J. M. Smith | |
149 | %A P. Y.\(hyT. Chang | |
150 | %T Optimizing the Performance of a Relational Algebra Database Interface | |
151 | %J Comm. Assoc. Comp. Mach. | |
152 | %K acm cacm | |
153 | %V 18 | |
154 | %N 10 | |
155 | %D October 1975 | |
156 | ||
157 | %A M. Stonebraker | |
158 | %A L. A. Rowe | |
159 | %T Observations on Data Manipulation Languages and their | |
160 | Embedding in General Purpose Programming Languages | |
161 | %R TR UCB/ERL M77-53 | |
162 | %D July 1977 | |
163 | %I University of California, Berkeley | |
164 | ||
165 | %A E. Wong | |
166 | %A K. Youssefi | |
167 | %T Decomposition \(em a Strategy for Query Processing | |
168 | %J ACM Trans. Data Base Systems | |
169 | %V 1 | |
170 | %N 3 | |
171 | %D September 1976 | |
172 | %P 223-241 | |
173 | ||
174 | %A C. Zaniolo | |
175 | %T Analysis and Design of Relational Schemata for Database Systems | |
176 | %R Tech. Rept. UCLA-ENG-7769 | |
177 | %I Department of Computer Science, UCLA | |
178 | %D July 1976 | |
179 | ||
180 | %A M. M. Zloof | |
181 | %T Query-by-Example: the Invocation and Definition of Tables and Forms | |
182 | %J Proc. ACM International Conf. on Very Large Data Bases | |
183 | %D September 1975 | |
184 | %P 1-24 | |
185 | ||
186 | %A S. K. Abdali | |
187 | %T A lambda calculus model of programming languages \(em I. simple constructs | |
188 | %J J. Comp. Languages | |
189 | %V 1 | |
190 | %D 1976 | |
191 | %P 287-301 | |
192 | ||
193 | %A S. K. Abdali | |
194 | %T A lambda calculus model of programming languages \(em II. jumps and procedures | |
195 | %J J. Comp. Languages | |
196 | %V 1 | |
197 | %D 1976 | |
198 | %P 303-320 | |
199 | ||
200 | %A ADJ (J. A. Goguen, J. W. Thatcher, E. G. Wagner and J. B Wright) | |
201 | %T A junction between category theory and computer science, I: basic concepts and examples (Part 1) | |
202 | %R Report RC 4526 | |
203 | %I IBM Research | |
204 | %C Yorktown Heights, N. Y. | |
205 | %K part1 | |
206 | %D September 1973 | |
207 | ||
208 | %A ADJ (J. A. Goguen, J. W. Thatcher, E. G. Wagner and J. B Wright) | |
209 | %T A junction between category theory and computer science, I: basic concepts and examples (Part 2) | |
210 | %R Report RC 5908 | |
211 | %I IBM Research | |
212 | %K part2 | |
213 | %C Yorktown Heights, N. Y. | |
214 | %D March 1976 | |
215 | ||
216 | %A L. Ammeraal | |
217 | %T How program statements transform predicates | |
218 | %R Report IW 39/75 | |
219 | %I Mathematisch Centrum | |
220 | %C Amsterdam | |
221 | %D December 1975 | |
222 | ||
223 | %A L. Ammeraal | |
224 | %T On forward and backward proof rules for program verification | |
225 | %R Report IW 65/76 | |
226 | %I Mathematisch Centrum | |
227 | %C Amsterdam | |
228 | %D November 1976 | |
229 | ||
230 | %A E. R. Anderson | |
231 | %A F. C. Belz | |
232 | %A E. K. Blum | |
233 | %T Semanol (73) A metalanguage for programming the semantics of programming languages | |
234 | %J Acta Informatica | |
235 | %V 6 | |
236 | %D 1976 | |
237 | %P 109-131 | |
238 | ||
239 | %A K. R. Apt | |
240 | %T Equivalence of operational and denotational semantics for a fragment of Pascal | |
241 | %R Report IW 71/76 | |
242 | %I Mathematisch Centrum | |
243 | %C Amsterdam | |
244 | %D December 1976 | |
245 | ||
246 | %A K. R. Apt | |
247 | %A J. W. de Bakker | |
248 | %T Exercises in denotational semantics | |
249 | %J Lecture Notes in Computer Science | |
250 | %V 45 | |
251 | %D 1976 | |
252 | %P 1-11 | |
253 | ||
254 | %A K. R. Apt | |
255 | %A J. W. de Bakker | |
256 | %T Semantics and proof theory of Pascal procedures | |
257 | %J Lecture Notes in Computer Science | |
258 | %V 52 | |
259 | %D 1977 | |
260 | %P 30-44 | |
261 | ||
262 | %A K. R. Apt | |
263 | %A L. G. L. T. Meertens | |
264 | %T Completeness with finite systems of intermediate assertions for recursive program schemas | |
265 | %R Report IW 84/77 | |
266 | %I Mathematisch Centrum | |
267 | %C Amsterdam | |
268 | %D September 1977 | |
269 | ||
270 | %A A. Arnold | |
271 | %A M. Nivat | |
272 | %T Non deterministic recursive program schemes | |
273 | %D 1977 | |
274 | ||
275 | %A A. Arnold | |
276 | %A M. Nivat | |
277 | %T On nondeterministic program schemes | |
278 | %D 1977 | |
279 | ||
280 | %A E. A. Ashcroft | |
281 | %A Maurice Clint | |
282 | %A C. A. R. Hoare | |
283 | %T Remarks on ``Program proving: jumps and functions by M. Clint and C. A. R. Hoare'' | |
284 | %J Acta Informatica | |
285 | %V 6 | |
286 | %D 1976 | |
287 | %P 317-318 | |
288 | ||
289 | %A J. W. Backus | |
290 | %A R. J. Beeber | |
291 | %A S. Best | |
292 | %A R. Goldberg | |
293 | %A L. M. Haibt | |
294 | %A H. L. Herrick | |
295 | %A R. A. Nelson | |
296 | %A D. Sayre | |
297 | %A P. B. Sheridan | |
298 | %A H. Stern | |
299 | %A I. Ziller | |
300 | %A R. A. Hughes | |
301 | %A R. Nutt | |
302 | %T The Fortran automatic coding system | |
303 | %J Western Computer Proceedings | |
304 | %D 1957 | |
305 | %P 188-198 | |
306 | ||
307 | %A J. P. Banatre | |
308 | %T Producing optimised code for coercions | |
309 | %J Information Processing Letters | |
310 | %V 6 | |
311 | %N 2 | |
312 | %D April 1977 | |
313 | %P 56-59 | |
314 | ||
315 | %A Henk Barendregt | |
316 | %T A global representation of the recursive functions in the $lambda -$claculus | |
317 | %J Theor. Comp. Sci. | |
318 | %V 3 | |
319 | %D 1976 | |
320 | %P 225-242 | |
321 | ||
322 | %A H. Bekic | |
323 | %T Towards a mathematical theory of processes | |
324 | %R TR 25.125 | |
325 | %I IBM Laboratory | |
326 | %C Vienna | |
327 | %D December 1971 | |
328 | ||
329 | %A G. Berry | |
330 | %T Bottom-up computation of recursive programs | |
331 | %R Rapport de Recherche No 133 | |
332 | %I IRIA | |
333 | %C Rocquencourt, France | |
334 | %D September 1975 | |
335 | ||
336 | %A Gerard Berry | |
337 | %A Bruno Courcelle | |
338 | %T Program equivalence and canonical forms in stable discrete interpretations | |
339 | %E S. Michaelson and R. Milner | |
340 | %B Automata Languages and Programming , Third International Colloquium | |
341 | %I Edinburgh University Press | |
342 | %D July 1976 | |
343 | %P 168-188 | |
344 | ||
345 | %A Gerard Berry | |
346 | %A J. J. Levy | |
347 | %T Minimal and optimal computations of recursive programs | |
348 | %J J. Assoc. Comp. Mach. | |
349 | %K acm jacm | |
350 | %D to appear | |
351 | ||
352 | %A Richard Bird | |
353 | %T Programs and Machines | |
354 | %I John Wiley | |
355 | %C New York, N. Y. | |
356 | %D 1976 | |
357 | ||
358 | %A A. Blikle | |
359 | %T Programs with subscripted variables | |
360 | %J Bulletin de L'Academie Polonaise des Sciences, Serie des sciences math., astr. et phys. | |
361 | %V XIX | |
362 | %N 9 | |
363 | %D 1971 | |
364 | %P 853-857 | |
365 | ||
366 | %A C. Bohm | |
367 | %T The CUCH as a formal and description language | |
368 | %E T. B. Steel, Jr. | |
369 | %B Formal language description languages for computer programming | |
370 | %I North-Holland | |
371 | %C Amsterdam | |
372 | %D 1966 | |
373 | %P 179-197 | |
374 | ||
375 | %A H. J. Boom | |
376 | %T Extended type checking | |
377 | %R Report IW 60/76 | |
378 | %I Mathematisch Centrum | |
379 | %C Amsterdam | |
380 | %D September 1976 | |
381 | ||
382 | %A S. R. Bourne | |
383 | %A A. D. Birrell | |
384 | %A I. Walker | |
385 | %T Algol 68C Reference Manual | |
386 | %I Computer Laboratory, Cambridge University | |
387 | %C Cambridge, England | |
388 | %D 1975 | |
389 | ||
390 | %A R. S. Boyer | |
391 | %A J. S. Moore | |
392 | %T A computer proof of the correctness of a simple optimizing compiler for expressions | |
393 | %R Tech. Rep. 5 | |
394 | %I SRI | |
395 | %C Menlo Park, Ca. | |
396 | %D January 1977 | |
397 | ||
398 | %A J. M. Boyle | |
399 | %A A. A. Grau | |
400 | %T An algorithmic semantics for Algol 60 identifier denotation | |
401 | %J J. Assoc. Comp. Mach. | |
402 | %K acm jacm | |
403 | %V 17 | |
404 | %N 2 | |
405 | %D April 1970 | |
406 | %P 361-382 | |
407 | ||
408 | %A R. M. Burstall | |
409 | %T Semantics of assignment | |
410 | %E Ella Dale and Donald Michie | |
411 | %B Machine Intelligence 2 | |
412 | %I American Elsevier | |
413 | %C New York | |
414 | %D 1968 | |
415 | %P 3-20 | |
416 | ||
417 | %A R. M. Burstall | |
418 | %T Proving properties of programs by structural induction | |
419 | %J Comp. J. | |
420 | %P 41-48 | |
421 | ||
422 | %A R. M. Burstall | |
423 | %T Some techniques for proving properties of programs which alter data structures | |
424 | %B Machine Intelligence | |
425 | ||
426 | %A E. M. Clarke, Jr. | |
427 | %T Program invariants as fixed points | |
428 | %J Proc. 18th IEEE Symp. on Foundations of Computer Science | |
429 | %D October 1977 | |
430 | %P 18-29 | |
431 | ||
432 | %A Maurice Clint | |
433 | %T Program proving: coroutines | |
434 | %J Acta Informatica | |
435 | %V 2 | |
436 | %N 1 | |
437 | %D 1973 | |
438 | %P 50-63 | |
439 | ||
440 | %A Maurice Clint | |
441 | %A C. A. R. Hoare | |
442 | %T Program proving:jumps and functions | |
443 | %J Acta Informatica | |
444 | %V 1 | |
445 | %D 1972 | |
446 | %P 214-224 | |
447 | %O see also Ashcroft, Clint and Hoare (1976) | |
448 | ||
449 | %A S. A. Cook | |
450 | %T Soundness and completeness of an axiom system for program verification | |
451 | %J SIAM J. Computing | |
452 | %D to appear | |
453 | ||
454 | %A S. A. Cook | |
455 | %A D. C. Oppen | |
456 | %T An assertion language for data structures | |
457 | %J Proc. 2nd ACM Symp. on Principles of Programming Languages | |
458 | %D January 1975 | |
459 | %P 160-166 | |
460 | ||
461 | %A D. C. Cooper | |
462 | %T Program scheme equivalences and second-order logic | |
463 | %B Machine Intelligence | |
464 | %P 3-15 | |
465 | ||
466 | %A Bruno Courcelle | |
467 | %T On the definition of classes of interpretations | |
468 | %R Rapport de Recherche No 231 | |
469 | %I IRIA | |
470 | %C Rocquencourt, France | |
471 | %D May 1977 | |
472 | ||
473 | %A B. Courcelle | |
474 | %A I. Guessarian | |
475 | %T On some classes of interpretations | |
476 | %R Rapport de Recherche No 253 | |
477 | %I IRIA | |
478 | %C Rocquencourt, France | |
479 | %D September 1977 | |
480 | ||
481 | %A Bruno Courcelle | |
482 | %A Jean Vuillemin | |
483 | %T Completeness results for the equivalence of recursive schema | |
484 | %J J. Comp. Sys. Sci. | |
485 | %V 12 | |
486 | %D 1976 | |
487 | %P 179-197 | |
488 | ||
489 | %A Karel Culik II | |
490 | %T A model for the formal definition of programming languages | |
491 | %J Int. J. Comp. Math. | |
492 | %V 3 | |
493 | %D 1973 | |
494 | %P 315-345 | |
495 | ||
496 | %A R. J. Cunningham | |
497 | %A M. E. J. Guilford | |
498 | %T A note on the semantic definition of side effects | |
499 | %J Information Processing Letters | |
500 | %V 4 | |
501 | %N 5 | |
502 | %D February 1976 | |
503 | %P 118-120 | |
504 | ||
505 | %A Ole-Johan Dahl | |
506 | %A Bjorn Myhrhaug | |
507 | %A Kristen Nygaard | |
508 | %T Simula 67: common base language | |
509 | %R Publication S-22 | |
510 | %I Norwegian Computing Centre | |
511 | %C Oslo, Norway | |
512 | %D October 1970 | |
513 | ||
514 | %A J. W. de Bakker | |
515 | %T Semantics of programming languages | |
516 | %E J. T. Tou | |
517 | %B Advances in Information Systems Science, Vol. 2 | |
518 | %I Plenum Press | |
519 | %C New York, N. Y. | |
520 | %D 1969 | |
521 | %P 173-227 | |
522 | ||
523 | %A J. W. de Bakker | |
524 | %T Recursive Procedures | |
525 | %I Mathem\ 1atical Centre Tracts 24, Mathematisch Centrum | |
526 | %C Amsterdam | |
527 | %D 1971 | |
528 | ||
529 | %A J. W. de Bakker | |
530 | %T Recursion, induction and symbol manipulation | |
531 | %B Informatica Symposium 1971 | |
532 | %I Mathematisch Centre Tracts 25, Mathematisch Centrum | |
533 | %D 1971 | |
534 | ||
535 | %A J. W. de Bakker | |
536 | %T Axiom systems for simple assignment statements | |
537 | %J Lecture Notes in Mathematics | |
538 | %V 188 | |
539 | %D 1971 | |
540 | %P 1-22 | |
541 | ||
542 | %A J. W. de Bakker | |
543 | %T A property of linear conditionals | |
544 | %J Lecture Notes in Mathematics | |
545 | %V 188 | |
546 | %D 1971 | |
547 | %P 23-27 | |
548 | ||
549 | %A J. W. de Bakker | |
550 | %T The fixpoint approach in semantics: theory and applications | |
551 | %E J. W. de Bakker | |
552 | %B Foundations of Computer Science | |
553 | %I Mathematical Centre Tracts 63 | |
554 | %C Amsterdam | |
555 | %D 1975 | |
556 | %P 3-53 | |
557 | ||
558 | %A J. W. de Bakker | |
559 | %T Least fixed points revisited | |
560 | %J Theor. Comp. Sci. | |
561 | %V 2 | |
562 | %D 1976 | |
563 | %P 155-181 | |
564 | ||
565 | %A J. W. de Bakker | |
566 | %A J. W. de Bakker | |
567 | %T Fixed point semantics and Dijkstra's fundamental invariance theorem | |
568 | %R Report IW 29/76 | |
569 | %I Mathematisch centrum | |
570 | %C Amsterdam | |
571 | %D January 1976 | |
572 | ||
573 | %A J. W. de Bakker | |
574 | %T Correctness proofs for assignment statements | |
575 | %R Report IW 55/76 | |
576 | %I Mathematisch Centrum | |
577 | %C Amsterdam | |
578 | %D 1976 | |
579 | ||
580 | %A J. W. de Bakker | |
581 | %T Semantics and the foundations of program proving | |
582 | %E B. Gilchrist | |
583 | %B Information Processing 77 | |
584 | %I North-Holland | |
585 | %C Amsterdam | |
586 | %D 1977 | |
587 | %P 279-284 | |
588 | ||
589 | %A J. W. de Bakker | |
590 | %T Recursive programs as predicate transformers | |
591 | %E E. Neuhold | |
592 | %B IFIP Working Conference on the Formal Description of Programming Concepts | |
593 | %I North-Holland | |
594 | %C Amsterdam | |
595 | %D to appear | |
596 | ||
597 | %A J. W. de Bakker | |
598 | %A L. G. L. T. Meertens | |
599 | %T On the completeness of the inductive assertion method | |
600 | %J J. Comp. Sys. Sci. | |
601 | %V 11 | |
602 | %D 1975 | |
603 | %P 323-357 | |
604 | ||
605 | %A J. W. de Bakker | |
606 | %A Dana Scott | |
607 | %T A theory of programs | |
608 | %R unpublished | |
609 | %D August 1969 | |
610 | ||
611 | %A Mariangiola Dezani-Ciancaglini | |
612 | %A Maddalena Zacchi | |
613 | %T Application of Church-Rosser properties to increase the parallelism and efficiency of algorithms | |
614 | %J Lecture Notes in Computer Science | |
615 | %V 14 | |
616 | %D 1974 | |
617 | ||
618 | %A E. W. Dijkstra | |
619 | %T A Discipline of Programming | |
620 | %I Prentice Hall | |
621 | %C Englewood Cliffs, N. J. | |
622 | %D 1976 | |
623 | ||
624 | %A J. E. Donahue | |
625 | %T The mathematical semantics of axiomatically defined programming language constructs | |
626 | %E G. Huet and G. Kahn | |
627 | %B Proving and Improving Programs | |
628 | %I IRIA | |
629 | %C Rocquencourt, France | |
630 | %D July 1975 | |
631 | %P 353-367 | |
632 | ||
633 | %A J. E. Donahue | |
634 | %T Complementary Definitions of Programming Language Semantics | |
635 | %J Lecture Notes in Computer Science | |
636 | %V 42 | |
637 | %D 1976 | |
638 | ||
639 | %A J. E. Donahue | |
640 | %T Locations considered unnecessary | |
641 | %J Acta Informatica | |
642 | %V 8 | |
643 | %D 1977 | |
644 | %P 221-242 | |
645 | ||
646 | %A H. Egli | |
647 | %T A mathematical model for non-deterministic computations | |
648 | %D September 1975 | |
649 | ||
650 | %A Herbert Egli | |
651 | %A Robert L. Constable | |
652 | %T Computability concepts for programming language semantics | |
653 | %J Theor. Comp. Sci. | |
654 | %V 2 | |
655 | %D 1976 | |
656 | %P 133-145 | |
657 | ||
658 | %A G. W. Ernst | |
659 | %T Rules of inference for procedure calls | |
660 | %J Acta Informatica | |
661 | %V 8 | |
662 | %D 1977 | |
663 | %P 145-152 | |
664 | ||
665 | %A R. W. Floyd | |
666 | %T Assigning meanings to programs | |
667 | %E J. T. Schwartz | |
668 | %B Mathematical Aspects of Computer Science, Proceedings of a Symposium in Applied Mathematics, Vol. 19 | |
669 | %I American Math. Soc. | |
670 | %C Providence, R. I. | |
671 | %D 1967 | |
672 | %P 19-32 | |
673 | ||
674 | %A Nissim Francez | |
675 | %A Boris Klebansky | |
676 | %A Amir Pnueli | |
677 | %T Backtracking in recursive computations | |
678 | %J Acta Informatica | |
679 | %V 8 | |
680 | %D 1977 | |
681 | %P 125-144 | |
682 | ||
683 | %A Jan V. Garwick | |
684 | %T The definition of programming languages by their compilers | |
685 | %E T. B. Steel, Jr. | |
686 | %B Formal Language Description Languages for Computer Programming | |
687 | %I North-Holland | |
688 | %C Amsterdam | |
689 | %D 1966 | |
690 | %P 139-147 | |
691 | ||
692 | %A Michael Gordon | |
693 | %T Operational reasoning and denotational semantics | |
694 | %E G. Huet and G. Kahn | |
695 | %B Proving and Improving Programs | |
696 | %I IRIA | |
697 | %C Rocquencourt, France | |
698 | %D July 1975 | |
699 | %P 83-98 | |
700 | ||
701 | %A G. A. Gorelick | |
702 | %T A complete axiomatic system for proving assertions about recursive and nonrecursive programs | |
703 | %R Tech. Rep. 75 | |
704 | %I Department of Computer Science, University of Toronto | |
705 | %D January 1975 | |
706 | ||
707 | %A David Gries | |
708 | %T Assignment to subscripted variables | |
709 | %R TR 77-305 | |
710 | %I Department of Computer Science, Cornell University | |
711 | %D September 1976 | |
712 | ||
713 | %A David Gries | |
714 | %T An illustration of current ideas on the derivation of correctness proofs and correct programs | |
715 | %J IEEE Trans. on Software Engineering | |
716 | %V SE-2 | |
717 | %N 4 | |
718 | %D December 1976 | |
719 | %P 238-244 | |
720 | ||
721 | %A David Gries | |
722 | %A Narain Gehani | |
723 | %T Some ideas on data types in high level languages | |
724 | %J Comm. Assoc. Comp. Mach. | |
725 | %K acm cacm | |
726 | %V 20 | |
727 | %N 6 | |
728 | %D July 1976 | |
729 | %P 414-420 | |
730 | ||
731 | %A D. Grune | |
732 | %T A view of coroutines | |
733 | %R Report IW 63/76 | |
734 | %I Mathematisch Centrum | |
735 | %C Amsterdam | |
736 | %D November 1976 | |
737 | ||
738 | %A Irene Guessarian | |
739 | %T Semantic equivalence of program schemes and its syntactic characterization | |
740 | %E S. Michaelson and R. Milner | |
741 | %B Automata, Languages and Programming, Third International Colloquium | |
742 | %I Edinburgh University Press | |
743 | %D July 1976 | |
744 | %P 189-200 | |
745 | ||
746 | %A I. Guessarian | |
747 | %T Sur quelques applications de la semantique algebrique des schemas recursifs polyadiques | |
748 | %D 1977 | |
749 | ||
750 | %A John Guttag | |
751 | %T Abstract data types and the development of data structures | |
752 | %J Comm. Assoc. Comp. Mach. | |
753 | %K acm cacm | |
754 | %V 20 | |
755 | %N 6 | |
756 | %D July 1976 | |
757 | %P 396-404 | |
758 | ||
759 | %A J. V. Guttag | |
760 | %A Ellis Horowitz | |
761 | %A D. R. Musser | |
762 | %T Abstract data types and software validation | |
763 | %R Report ISI/RR-76-48 | |
764 | %I Information Sciences Institute, University of Southern California | |
765 | %C Los Angeles, Ca. | |
766 | %D August 1976 | |
767 | ||
768 | %A J. V. Guttag | |
769 | %A Ellis Horowitz | |
770 | %A D. R. Musser | |
771 | %T The design of data type specifications | |
772 | %R Report ISI/RR-76-49 | |
773 | %I Information Sciences Institute, Univeristy of Southern California | |
774 | %C Los Angeles, Ca. | |
775 | %D November 1976 | |
776 | ||
777 | %A D. Harel | |
778 | %T Arithmetical completeness in logics of programs | |
779 | %D September 1977 | |
780 | ||
781 | %A David Harel | |
782 | %T On the correctness of regular deterministic programs; a unifying survey | |
783 | %D November 1977 | |
784 | ||
785 | %A D. Harel | |
786 | %T Complete axiomatization of properties of recursive programs (extended abstract) | |
787 | %D November 1977 | |
788 | ||
789 | %A David Harel | |
790 | %A Amir Pnueli | |
791 | %A Jonathan Stavi | |
792 | %T A complete axiomatic system for proving deductions about recursive programs | |
793 | %J Ninth ACM Symp. Theory of Computing | |
794 | %D May 1977 | |
795 | %P 249-260 | |
796 | ||
797 | %A D. Harel | |
798 | %A V. R. Pratt | |
799 | %T Nondeterminism in logics of programs | |
800 | %J Proc. 5th ACM Symp. on Principles of Programming Languages | |
801 | %D January 1978 | |
802 | ||
803 | %A William Harrison | |
804 | %T Formal semantics of a schematic intermediate language | |
805 | %R Report RC 6271 | |
806 | %I IBM Research | |
807 | %C Yorktown Heights, N. Y. | |
808 | %D November 1976 | |
809 | ||
810 | %A R. Haskell | |
811 | %T Efficient implementation of a class of recursively defined functions | |
812 | %J Comp. J. | |
813 | %V 18 | |
814 | %N 1 | |
815 | %D 1975 | |
816 | %P 23-29 | |
817 | ||
818 | %A Peter Henderson | |
819 | %A J. H. Morris, Jr. | |
820 | %T A lazy evaluator | |
821 | %J Proc. 3rd ACM Symp. on Principles of Programming Languages | |
822 | %D January 1976 | |
823 | %P 95-103 | |
824 | ||
825 | %A M. C. B. Hennessy | |
826 | %T Parameter passing mechanisms and non-determinism | |
827 | ||
828 | %A M. C. B. Hennessy | |
829 | %A E. A. Ashcroft | |
830 | %T The semantics of nondeterminism | |
831 | %R Report CS-76-17 | |
832 | %I Department of Computer Science, University of Waterloo | |
833 | %D April 1976 | |
834 | ||
835 | %A C. A. R. Hoare | |
836 | %T An axiomatic basis for computer programming | |
837 | %J Comm. Assoc. Comp. Mach. | |
838 | %K acm cacm | |
839 | %V 12 | |
840 | %N 10 | |
841 | %D October 1969 | |
842 | %P 576-580,583 | |
843 | ||
844 | %A C. A. R. Hoare | |
845 | %T Procedures and parameters: an axiomatic approach | |
846 | %J Lecture Notes in Mathematics | |
847 | %V 188 | |
848 | %D 1971 | |
849 | %P 102-116 | |
850 | ||
851 | %A C. A. R. Hoare | |
852 | %T Proof of correctness of data representations | |
853 | %J Acta Informatica | |
854 | %V 1 | |
855 | %D 1972 | |
856 | %P 271-281 | |
857 | ||
858 | %A C. A. R. Hoare | |
859 | %T Hints on programming language design | |
860 | %O Invited address at ACM Symposium on Principles of Programming Languages. | |
861 | %D October 1973 | |
862 | ||
863 | %A C. A. R. Hoare | |
864 | %T Some properties of non-deterministic computations | |
865 | ||
866 | %A C. A. R. Hoare | |
867 | %A P. E. Lauer | |
868 | %T Consistent and complementary formal theories of the semantics of programming languages | |
869 | %J Acta Informatica | |
870 | %V 3 | |
871 | %D 1974 | |
872 | %P 135-153 | |
873 | ||
874 | %A C. M. Hoffman | |
875 | %T Design and correctness of a compiler for Lucid | |
876 | %R Research Report CS-76-20 | |
877 | %I Computer Science Department, University of Waterloo | |
878 | %D May 1976 | |
879 | ||
880 | %A C. M. Hoffman | |
881 | %A L. H. landweber | |
882 | %T A completeness theorem for straight-line programs with structured variables | |
883 | %J J. Assoc. Comp. Mach. | |
884 | %K acm jacm | |
885 | %V 23 | |
886 | %N 1 | |
887 | %D January 1976 | |
888 | %P 203-220 | |
889 | ||
890 | %A Chiharu Hosono | |
891 | %A Masahiko Sato | |
892 | %T The retracts in $P omega$ do not form a continuous lattice \(em a solution to Scott's problem | |
893 | %J Theor. Comp. Sci. | |
894 | %V 4 | |
895 | %D 1977 | |
896 | %P 137-142 | |
897 | ||
898 | %A Gerard Huet | |
899 | %T Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems | |
900 | %J Proc. 18th IEEE Symp. on Foundations of Computer Science | |
901 | %D October 1977 | |
902 | %P 30-45 | |
903 | ||
904 | %A Gerard Huet | |
905 | %A Bernard Lang | |
906 | %T Program transformations in classes of interpretations | |
907 | %O Lecture Notes | |
908 | %D May 1976 | |
909 | ||
910 | %A Shigeru Igarashi | |
911 | %T Semantics of Algol-like statements | |
912 | %J Lecture Notes in Mathematics | |
913 | %V 188 | |
914 | %D 1971 | |
915 | %P 117-177 | |
916 | ||
917 | %A Shigeru Igarashi | |
918 | %A R. L. London | |
919 | %A D. C. Luckham | |
920 | %T Automatic program verification I: a logical basis and its implementation | |
921 | %J Acta Informatica | |
922 | %V 4 | |
923 | %D 1975 | |
924 | %P 145-182 | |
925 | ||
926 | %A Kurt Jensen | |
927 | %T An investigation into different semantic approaches | |
928 | %R Report DAIMI PB-61 | |
929 | %I Department of Computer Science, University of Aarhus | |
930 | %D June 1976 | |
931 | ||
932 | %A Gilles Kahn | |
933 | %T An approach to systems correctness | |
934 | ||
935 | %A Gilles Kahn | |
936 | %T The semantics of a simple language for parallel programming | |
937 | %E J. L. Rosenfeld | |
938 | %B Information Processing 74 | |
939 | %I North-Holland | |
940 | %C Amsterdam | |
941 | %D 1974 | |
942 | %P 471-475 | |
943 | ||
944 | %A Gilles Kahn | |
945 | %A D. B. MacQueen | |
946 | %T Coroutines and networks of parallel processes | |
947 | %E B. Gilchrist | |
948 | %B Information Processing 77 | |
949 | %I North-Holland | |
950 | %C Amsterdam | |
951 | %D 1977 | |
952 | %P 993-998 | |
953 | ||
954 | %A D. M. Kaplan | |
955 | %T Some completeness results in the mathematical theory of computation | |
956 | %J J. Assoc. Comp. Mach. | |
957 | %K acm jacm | |
958 | %V 15 | |
959 | %N 1 | |
960 | %D January 1968 | |
961 | %P 124-134 | |
962 | ||
963 | %A R. M. Keller | |
964 | %T Denotational models for parallel programs with indeterminate operators | |
965 | %E E. Neuhold | |
966 | %B IFIP Working Conference on the Formal Description of Programming Concepts | |
967 | %I North-Holland | |
968 | %C Amsterdam | |
969 | %D to appear | |
970 | ||
971 | %A D. E. Knuth | |
972 | %A P. B. Bendix | |
973 | %T Simple word problems in universal algebras | |
974 | %E J. Leech | |
975 | %B Computational Problems in Abstract Algebra | |
976 | %I Pergamon Press | |
977 | %C Oxford | |
978 | %D 1970 | |
979 | %P 263-297 | |
980 | ||
981 | %A D. E. Knuth | |
982 | %A L. Trabb Pardo | |
983 | %T Early development of programming languages | |
984 | %B Encyclopedia of Computer Science and Technology, Vol. 7 | |
985 | %I Marcel Dekker | |
986 | %C New York, N. Y. | |
987 | %D 1977 | |
988 | %P 419-493 | |
989 | %R STAN-CS-76-562 | |
990 | ||
991 | %A J. Kral | |
992 | %T On the equivalence of modes and the equivalence of finite automata | |
993 | %J ALGOL Bulletin | |
994 | %N 35 | |
995 | %D March 1973 | |
996 | %P 34-35 | |
997 | ||
998 | %A P. J. Landin | |
999 | %T The mechanical evaluation of expressions | |
1000 | %J Comp. J. | |
1001 | %V 6 | |
1002 | %N 4 | |
1003 | %D January 1964 | |
1004 | %P 308-320 | |
1005 | ||
1006 | %A P. J. Landin | |
1007 | %T A correspondence between Algol 60 and Church's lambda-notation | |
1008 | %J Comm. Assoc. Comp. Mach. | |
1009 | %K acm cacm | |
1010 | %V 8 | |
1011 | %N 2,3 | |
1012 | %D February and March 1965 | |
1013 | %P 89-101 and 158-165 | |
1014 | ||
1015 | %A P. J. Landin | |
1016 | %T A formal description of Algol 60 | |
1017 | %E T. B. Steel, Jr. | |
1018 | %B Formal Language Description Languages for Computer Programming | |
1019 | %I North-Holland | |
1020 | %C Amsterdam | |
1021 | %D 1966 | |
1022 | %P 266-294 | |
1023 | ||
1024 | %A P. J. Landin | |
1025 | %T The next 700 programming languages | |
1026 | %J Comm. Assoc. Comp. Mach. | |
1027 | %K acm cacm | |
1028 | %V 9 | |
1029 | %N 3 | |
1030 | %D March 1966 | |
1031 | %P 157-166 | |
1032 | ||
1033 | %A P. J. Landin | |
1034 | %T A $lambda -$calculus approach | |
1035 | %E L. Fox | |
1036 | %B Advances in Programming and Non-numerical Computation | |
1037 | %I Pergammon Press | |
1038 | %C Oxford | |
1039 | %D 1966 | |
1040 | %P 97-141 | |
1041 | ||
1042 | %A Hans Langmaack | |
1043 | %T On correct procedure parameter transmission in higher programming languages | |
1044 | %J Acta Informatica | |
1045 | %V 2 | |
1046 | %D 1973 | |
1047 | %P 110-142 | |
1048 | ||
1049 | %A D. Lankford | |
1050 | %T On deciding word problems by rewrite rule simplifiers | |
1051 | %D September 1977 | |
1052 | ||
1053 | %A H. F. Ledgard | |
1054 | %T A model for type checking \(em with an application to Algol 60 | |
1055 | %J Comm. Assoc. Comp. Mach. | |
1056 | %K acm cacm | |
1057 | %V 15 | |
1058 | %N 11 | |
1059 | %D November 1972 | |
1060 | %P 956- | |
1061 | ||
1062 | %A J. A. N. Lee | |
1063 | %T The formal definition of the Basic language | |
1064 | %J Comp. J. | |
1065 | %V 15 | |
1066 | %N 1 | |
1067 | %D February 1972 | |
1068 | %P 37-41 | |
1069 | ||
1070 | %A D. J. Lehmann | |
1071 | %A M. B. Smyth | |
1072 | %T Data types | |
1073 | %J Proc. 18th IEEE Symp. on Foundations of Computer Science | |
1074 | %D October 1977 | |
1075 | %P 7-12 | |
1076 | ||
1077 | %A G. T. Ligler | |
1078 | %T Proof rules, mathematical semantics and programming language design | |
1079 | %D 1975 | |
1080 | ||
1081 | %A G. T. Ligler | |
1082 | %T Surface properties of programming language constructs | |
1083 | %J Theor. Comp. Sci. | |
1084 | %D to appear | |
1085 | ||
1086 | %A R. J. Lipton | |
1087 | %T A necessary and sufficient condition for the existence of Hoare logics | |
1088 | %J Proc. 18th IEEE Symp. on Foundations of Computer Science | |
1089 | %D October 1977 | |
1090 | %P 1-6 | |
1091 | ||
1092 | %A R. L. London | |
1093 | %T A bibliography on proving the correctness of programs | |
1094 | %E B. Meltzer | |
1095 | %E D. Michie | |
1096 | %B Machine Intelligence 5 | |
1097 | %I Edinburgh University Press, Edinburgh, and American Elsevier, New York, N. Y. | |
1098 | %D 1970 | |
1099 | %P 569-580 | |
1100 | ||
1101 | %A R. L. London | |
1102 | %A M. Shaw | |
1103 | %A W. A. Wulf | |
1104 | %T Abstraction and verification in Alphard: a symbol table example | |
1105 | %D December 1976 | |
1106 | ||
1107 | %A Peter Lucas | |
1108 | %T On the semantics of programming languages and software devices | |
1109 | %E R. Rustin | |
1110 | %B Formal Semantics of Programming Languages | |
1111 | %I Prentice-Hall | |
1112 | %C Englewood Cliffs, N. J. | |
1113 | %D 1972 | |
1114 | %P 41-57 | |
1115 | ||
1116 | %A P. Lucas | |
1117 | %T Formal definition of programming languages and systems | |
1118 | %B Information Processing 71 | |
1119 | %I North-Holland | |
1120 | %C Amsterdam | |
1121 | %D 1971 | |
1122 | %P 291-297 | |
1123 | ||
1124 | %A Peter Lucas | |
1125 | %A Kurt Walk | |
1126 | %T On the formal definition of PL/I | |
1127 | %J Annual Review of Automatic Programming | |
1128 | %V 6 | |
1129 | %N 3 | |
1130 | %D 1970 | |
1131 | %P 105-182 | |
1132 | ||
1133 | %A D. C. Luckham | |
1134 | %A D. M. R. Park | |
1135 | %A M. S. Paterson | |
1136 | %T On formalized computer programs | |
1137 | %J J. Comp. Sys. Sci. | |
1138 | %V 4 | |
1139 | %D 1970 | |
1140 | %P 220-249 | |
1141 | ||
1142 | %A D. C. Luckham | |
1143 | %A Norihisa Suzuki | |
1144 | %T Automatic program verification V: verification oriented proof rules for arrays, records and pointers | |
1145 | %R Report STAN-CS-76-549 | |
1146 | %D March 1976 | |
1147 | ||
1148 | %A D. C. Luckham | |
1149 | %A Norihisa Suzuki | |
1150 | %T Proof of termination within a weak logic of programs | |
1151 | %J Acta Informatica | |
1152 | %V 8 | |
1153 | %D 1977 | |
1154 | %P 21-36 | |
1155 | ||
1156 | %A M. E. Majster | |
1157 | %T Extended data graphs, a formalism for structured data and data structures | |
1158 | %J Acta Informatica | |
1159 | %V 8 | |
1160 | %D 1977 | |
1161 | %P 37-59 | |
1162 | ||
1163 | %A Zohar Manna | |
1164 | %A Stephen Ness | |
1165 | %A Jean Vuillemin | |
1166 | %T Inductive methods for proving properties of programs | |
1167 | %J Comm. Assoc. Comp. Mach. | |
1168 | %K acm cacm | |
1169 | %V 16 | |
1170 | %N 8 | |
1171 | %D August 1973 | |
1172 | %P 491-502 | |
1173 | ||
1174 | %A Zohar Manna | |
1175 | %A Jean Vuillemin | |
1176 | %T Fixpoint approach to the theory of computation | |
1177 | %J Comm. Assoc. Comp. Mach. | |
1178 | %K acm cacm | |
1179 | %V 15 | |
1180 | %N 7 | |
1181 | %D July 1972 | |
1182 | %P 528-536 | |
1183 | ||
1184 | %A George Markowsky | |
1185 | %T categories of chain-complete posets | |
1186 | %J Theor. Comp. Sci. | |
1187 | %V 4 | |
1188 | %D 1977 | |
1189 | %P 125-135 | |
1190 | ||
1191 | %A G Markowsky | |
1192 | %A B. K. Rosen | |
1193 | %T Bases for chain-complete posets | |
1194 | %J IBM J. Research and Development | |
1195 | %V 20 | |
1196 | %N 2 | |
1197 | %D March 1976 | |
1198 | %P 138-147 | |
1199 | ||
1200 | %A W. D. Maurer | |
1201 | %T Induction principles for context-free languages | |
1202 | %J Lecture Notes in Computer Science | |
1203 | %V 1 | |
1204 | %D 1973 | |
1205 | %P 134-143 | |
1206 | ||
1207 | %A John McCarthy | |
1208 | %T Recursive functions of symbolic expressions and their computation by machine, part I | |
1209 | %J Comm. Assoc. Comp. Mach. | |
1210 | %K acm cacm | |
1211 | %V 3 | |
1212 | %N 4 | |
1213 | %D April 1960 | |
1214 | %P 184-195 | |
1215 | ||
1216 | %A John McCarthy | |
1217 | %T Towards a mathematical science of computation | |
1218 | %E C. M. Popplewell | |
1219 | %B Information Processing 1962 | |
1220 | %I North-Holland | |
1221 | %C Amsterdam | |
1222 | %D 1963 | |
1223 | %P 21-28 | |
1224 | ||
1225 | %A John McCarthy | |
1226 | %T A basis for a mathematical theory of computation | |
1227 | %E P. Braffort and D. Hirschberg | |
1228 | %B Computer Programming and Formal Systems | |
1229 | %I North-Holland | |
1230 | %C Amsterdam | |
1231 | %D 1963 | |
1232 | %P 33-70 | |
1233 | ||
1234 | %A John McCarthy | |
1235 | %T A formal description of a subset of Algol | |
1236 | %E T. B. Steel, Jr. | |
1237 | %B Formal Language Description Languages for Computer Programming | |
1238 | %I North-Holland | |
1239 | %C Amsterdam | |
1240 | %D 1966 | |
1241 | %P 1-12 | |
1242 | ||
1243 | %A John McCarthy | |
1244 | %A James Painter | |
1245 | %T Correctness of a compiler for arithmetic expressions | |
1246 | %E J. T. Schwartz | |
1247 | %B Proceedings of Symposia in Applied Mathematics, Volume XIX | |
1248 | %I American Math. Society | |
1249 | %C Providence, R. I. | |
1250 | %D 1967 | |
1251 | %P 33-41 | |
1252 | ||
1253 | %A M. D. McIlroy | |
1254 | %T Coroutines | |
1255 | %D 1968 | |
1256 | ||
1257 | %A Robert Milne | |
1258 | %T Verifying the correctness of implementations | |
1259 | %D 1977 | |
1260 | ||
1261 | %A R. E. Milne | |
1262 | %T Transforming predicate transformers | |
1263 | %E E. Neuhold | |
1264 | %B IFIP Working Conference on the Formal Description of Programming Concepts | |
1265 | %I North-Holland | |
1266 | %C Amsterdam | |
1267 | %D to appear | |
1268 | ||
1269 | %A Robin Milner | |
1270 | %T Models in LCF | |
1271 | %R Report STAN-CS-73-332 | |
1272 | %I Computer Science Department, Stanford University | |
1273 | %D January 1973 | |
1274 | ||
1275 | %A R. Milner | |
1276 | %T Processes; a model of computing agents | |
1277 | ||
1278 | %A R. Milner | |
1279 | %T Program semantics and mechanized proof | |
1280 | %I Mathematical Centre Tracts 82 | |
1281 | %D 1976 | |
1282 | %P 3-44 | |
1283 | ||
1284 | %A R. Milner | |
1285 | %T LCF; a methodology for performing rigorous proofs about programs | |
1286 | %B First IBM Symposium on Mathematical Foundations of Computer Science | |
1287 | %I Academic and Scientific Programs, IBM Japan | |
1288 | %C Tokyo | |
1289 | %D October 1976 | |
1290 | ||
1291 | %A J. H. Morris, Jr. | |
1292 | %T Another recursion induction principle | |
1293 | %J Comm. Assoc. Comp. Mach. | |
1294 | %K acm cacm | |
1295 | %V 14 | |
1296 | %N 5 | |
1297 | %D May 1971 | |
1298 | %P 351-354 | |
1299 | ||
1300 | %A P. D. Mosses | |
1301 | %T The mathematical semantics of Algol 60 | |
1302 | %R Technical Monograph PRG-12 | |
1303 | %I Programming Research Group, Oxford University | |
1304 | %D 1974 | |
1305 | ||
1306 | %A P. D. Mosses | |
1307 | %T The semantics of semantic equations | |
1308 | %J Lecture Notes in Computer Science | |
1309 | %V 28 | |
1310 | %D 1975 | |
1311 | %P 409-422 | |
1312 | ||
1313 | %A P. D. Mosses | |
1314 | %T Compiler generation using denotational semantics | |
1315 | %J Lecture Notes in Computer Science | |
1316 | %V 45 | |
1317 | %D 1976 | |
1318 | %P 436-441 | |
1319 | ||
1320 | %A P. D. Mosses | |
1321 | %T Making denotational semantics less concrete | |
1322 | %D 1977 | |
1323 | ||
1324 | %A Maurice Nivat | |
1325 | %T On some families of languages related to the Dyck language | |
1326 | %J Proc. 2nd ACM Symp. on Theory of Computing | |
1327 | %D May 1970 | |
1328 | %P 221-225 | |
1329 | ||
1330 | %A M. Nivat | |
1331 | %T On the interpretation of recursive program schemes | |
1332 | %R Rapport de Recherche No 84 | |
1333 | %I IRIA | |
1334 | %C Rocquencourt, France | |
1335 | %D October 1974 | |
1336 | ||
1337 | %A Mike O'Donnell | |
1338 | %T Subtree replacement systems: a unifying theory for recursive equations, Lisp, Lucid and combinatory logic | |
1339 | %J Ninth ACM Symp. Theory of Computing | |
1340 | %D May 1977 | |
1341 | %P 295-305 | |
1342 | ||
1343 | %A D. C. Oppen | |
1344 | %A S. A. Cook | |
1345 | %T Proving assertions about programs that manipulate data structures | |
1346 | %J Proc. 7th ACM Symp. on Theory of Computing | |
1347 | %D May 1975 | |
1348 | %P 107-116 | |
1349 | ||
1350 | %A B. A. Othmer | |
1351 | %T Programming language data structures: a comparative study | |
1352 | %R Tech. Rep. No. 30 | |
1353 | %I Department of Computer Science, Rutgers University | |
1354 | %D March 1974 | |
1355 | ||
1356 | %A G. Pacini | |
1357 | %T An optimal fix-point computation rule for a simple recursive language | |
1358 | %R Nota Interna B73-10 | |
1359 | %I Consiglio Nazionale delle Ricerche, Istituto di Elaborazione della Informazione | |
1360 | %C Pisa | |
1361 | %D October 1973 | |
1362 | ||
1363 | %A G. Pacini | |
1364 | %A C. Montangero | |
1365 | %A F. Turini | |
1366 | %T Graph representation and computation rules for typeless recursive languages | |
1367 | %J Lecture Notes in Computer Science | |
1368 | %V 14 | |
1369 | %D 1974 | |
1370 | %P 158-169 | |
1371 | ||
1372 | %A F. G. Pagan | |
1373 | %T On interpreter oriented definitions of programming languages | |
1374 | %J Comp. J. | |
1375 | %V 19 | |
1376 | %N 2 | |
1377 | %D 1976 | |
1378 | %P 151-155 | |
1379 | ||
1380 | %A David Park | |
1381 | %T Some semantics for data structures | |
1382 | %E D. Michie | |
1383 | %B Machine Intelligence 3 | |
1384 | %I American Elsevier | |
1385 | %C New York, N. Y. | |
1386 | %D 1968 | |
1387 | %P 351-371 | |
1388 | ||
1389 | %A David Park | |
1390 | %T Fixpoint induction and proofs of program properties | |
1391 | %B Machine Intelligence 5 | |
1392 | %D 1970 | |
1393 | %P 59-78 | |
1394 | ||
1395 | %A David Park | |
1396 | %T Finiteness is mu-ineffable | |
1397 | %J Theor. Comp. Sci. | |
1398 | %V 3 | |
1399 | %D 1976 | |
1400 | %P 173-181 | |
1401 | ||
1402 | %A Helmut Partsch | |
1403 | %A Peter Pepper | |
1404 | %T A family of rules for recursion removal | |
1405 | %J Information Processing Letters | |
1406 | %V 5 | |
1407 | %N 6 | |
1408 | %D December 1976 | |
1409 | %P 174-177 | |
1410 | ||
1411 | %A G. D. Plotkin | |
1412 | %T A set-theoretical definition of application | |
1413 | %R Memorandum MIP-R-95 | |
1414 | %I School of Artificial Intelligence, University of Edinburgh | |
1415 | %D March 1972 | |
1416 | ||
1417 | %A G. D. Plotkin | |
1418 | %T Lambda-definability and logical relations | |
1419 | %R Memorandum SAI-RM-4 | |
1420 | %I School of Artificial Intelligence, University of Edinburgh | |
1421 | %D October 1973 | |
1422 | ||
1423 | %A G. D. Plotkin | |
1424 | %T Call-by-name, call-by-value and the $lambda -$calculus | |
1425 | %J Theor. Comp. Sci. | |
1426 | %V 1 | |
1427 | %D 1975 | |
1428 | %P 125-159 | |
1429 | ||
1430 | %A A. Pnueli | |
1431 | %T The temporal logic of programs | |
1432 | %J Proc. 18th IEEE Symp. on Foundations of Computer Science | |
1433 | %D October 1977 | |
1434 | %P 46-57 | |
1435 | ||
1436 | %A V. R. Pratt | |
1437 | %T Semantical considerations in Floyd-Hoare logic | |
1438 | %J Proc. 17th IEEE Symp. on Foundations of Computer Science | |
1439 | %D October 1976 | |
1440 | %P 109-121 | |
1441 | ||
1442 | %A J. C. Raoult | |
1443 | %A J. Vuillemin | |
1444 | %T Operational and semantic equivalence between recursive programs | |
1445 | %D 1977 | |
1446 | ||
1447 | %A J. C. Reynolds | |
1448 | %T Relational and continuation semantics for a simple imperative language | |
1449 | %B Seminaires IRIA: theorie des algorithmes, des langages et de la programmation | |
1450 | %D 1974 | |
1451 | %P 51-58 | |
1452 | ||
1453 | %A J. C. Reynolds | |
1454 | %T On the relation between direct and continuation semantics | |
1455 | %J Lecture Notes in Computer Science | |
1456 | %V 14 | |
1457 | %D 1974 | |
1458 | %P 141-156 | |
1459 | ||
1460 | %A J. C. Reynolds | |
1461 | %T Formal semantics | |
1462 | %O preliminary draft for Cosers | |
1463 | %D June 1976 | |
1464 | ||
1465 | %A J. C. Reynolds | |
1466 | %T Semantics of the domain of flow diagrams | |
1467 | %J J. Assoc. Comp. Mach. | |
1468 | %K acm jacm | |
1469 | %V 24 | |
1470 | %N 3 | |
1471 | %D July 1977 | |
1472 | %P 484-503 | |
1473 | ||
1474 | %A H. G. Rice | |
1475 | %T Recursion and iteration | |
1476 | %J Comm. Assoc. Comp. Mach. | |
1477 | %K acm cacm | |
1478 | %V 8 | |
1479 | %N 2 | |
1480 | %D February 1965 | |
1481 | %P 114-115 | |
1482 | ||
1483 | %A J. S. Rohl | |
1484 | %T Converting a class of recursive procedures into non-recursive ones | |
1485 | %J Software \(em Practice and Experience | |
1486 | %V 7 | |
1487 | %D 1977 | |
1488 | %P 231-238 | |
1489 | ||
1490 | %A B. D. Russell | |
1491 | %T Implementation correctness involving a language with goto statements | |
1492 | %J SIAM J. Computing | |
1493 | %V 6 | |
1494 | %N 3 | |
1495 | %D September 1977 | |
1496 | %P 403-415 | |
1497 | ||
1498 | %A Bruce Russell | |
1499 | %T On an equivalence between continuation and stack semantics | |
1500 | %J Acta Informatica | |
1501 | %V 8 | |
1502 | %D 1977 | |
1503 | %P 113-123 | |
1504 | ||
1505 | %A Andrzej Salwicki | |
1506 | %T Procedures, formal computations and models | |
1507 | %J Lecture Notes in Computer Science | |
1508 | %V 28 | |
1509 | %D 1975 | |
1510 | %P 464-484 | |
1511 | ||
1512 | %A J. G. Sanderson | |
1513 | %T The lambda calculus, lattice theory and reflexive domains | |
1514 | %D 1973 | |
1515 | ||
1516 | %A E. Sciore | |
1517 | %A A. Tang | |
1518 | %T Computability theory in admissible domains | |
1519 | %D 1977 | |
1520 | ||
1521 | %A Dana Scott | |
1522 | %T Outline of a mathematical theory of computation | |
1523 | %J Proc. 4th Princeton Conf. on Information Sciences and Systems | |
1524 | %D March 1970 | |
1525 | %P 169-176 | |
1526 | ||
1527 | %A Dana Scott | |
1528 | %T The lattice of flow diagrams | |
1529 | %J Lecture Notes in Mathematics | |
1530 | %V 188 | |
1531 | %D 1971 | |
1532 | %P 311-366 | |
1533 | ||
1534 | %A Dana Scott | |
1535 | %T Continuous lattices | |
1536 | %E F. W. Lawvere | |
1537 | %B Toposes, Algebraic Geometry and Logic | |
1538 | %I Lecture Notes in Mathematics 274, Springer Verlag | |
1539 | %C Berlin | |
1540 | %D 1972 | |
1541 | %P 97-136 | |
1542 | ||
1543 | %A Dana Scott | |
1544 | %T Mathematical concepts in programming language semantics | |
1545 | %J Proc. AFIPS SJCC | |
1546 | %D 1972 | |
1547 | %P 225-234 | |
1548 | ||
1549 | %A Dana Scott | |
1550 | %T A simplified construction for $lambda -$calculus models | |
1551 | %C Uppsala | |
1552 | %D April 1973 | |
1553 | ||
1554 | %A Dana Scott | |
1555 | %T Data types as lattices | |
1556 | %J SIAM J. Computing | |
1557 | %V 5 | |
1558 | %N 3 | |
1559 | %D September 1976 | |
1560 | %P 522-587 | |
1561 | ||
1562 | %A Dana Scott | |
1563 | %T Logic and programming languages | |
1564 | %J Comm. Assoc. Comp. Mach. | |
1565 | %K acm cacm | |
1566 | %V 20 | |
1567 | %N 9 | |
1568 | %D September 1977 | |
1569 | %P 634-640 | |
1570 | ||
1571 | %A Dana Scott | |
1572 | %A Christopher Strachey | |
1573 | %T Towards a mathematical semantics for computer languages | |
1574 | %B Proceedings of the Symposium on Computers and Automata | |
1575 | %I Polytechnic Press | |
1576 | %C Brooklyn, N. Y. | |
1577 | %D April 1971 | |
1578 | %P 19-46 | |
1579 | ||
1580 | %A Adi Shamir | |
1581 | %A W. W. Wadge | |
1582 | %T Data types as objects | |
1583 | %J Lecture Notes in Computer Science | |
1584 | %V 52 | |
1585 | %D 1977 | |
1586 | %P 465-479 | |
1587 | ||
1588 | %A M. Shaw | |
1589 | %A W. A. Wulf | |
1590 | %A R. L. London | |
1591 | %T Abstraction and verification in Alphard: iteration and generators | |
1592 | %R Report ISI/RR-76-47 | |
1593 | %I Information Sciences Institute, University of Southern California | |
1594 | %C Los Angeles | |
1595 | %D August 1976 | |
1596 | ||
1597 | %A M. B. Smyth | |
1598 | %T Powerdomains | |
1599 | %D 1977 | |
1600 | ||
1601 | %A M. B. Smyth | |
1602 | %A G. D. Plotkin | |
1603 | %T The category-theoretic solution of recursive domain equations | |
1604 | %J Proc. 18th IEEE Symp. on Foundations of Computer Science | |
1605 | %D October 1977 | |
1606 | %P 13-17 | |
1607 | ||
1608 | %A J. E. Stoy | |
1609 | %T The congruence of two programming language definitions | |
1610 | %J Theor. Comp. Sci. | |
1611 | %D to appear | |
1612 | ||
1613 | %A Christopher Strachey | |
1614 | %T Towards a formal semantics | |
1615 | %E T. B. Steel, Jr. | |
1616 | %B Formal Language Description Languages for Computer Programming | |
1617 | %I North-Holland | |
1618 | %C Amsterdam | |
1619 | %D 1966 | |
1620 | %P 198-220 | |
1621 | ||
1622 | %A Christopher Strachey | |
1623 | %T Varieties of programming language | |
1624 | %B International Computing Symposium Proceedings | |
1625 | %I Cini Foundation | |
1626 | %C Venice | |
1627 | %D April 1972 | |
1628 | %P 222-233 | |
1629 | ||
1630 | %A Christopher Strachey | |
1631 | %A Christopher Wadsworth | |
1632 | %T Continuations: a mathematical semantics which can deal with full jumps | |
1633 | %R Technical Monograph PRG-11 | |
1634 | %I Programming Research Group, Oxford University | |
1635 | %D 1974 | |
1636 | ||
1637 | %A A. Tang | |
1638 | %T Chain properties in P$omega$ | |
1639 | %D 1977 | |
1640 | ||
1641 | %A Alfred Tarski | |
1642 | %T A lattice-theoretical fixpoint theorem and its applications | |
1643 | %J Pacific J. Math. | |
1644 | %V 5 | |
1645 | %N 2 | |
1646 | %D June 1955 | |
1647 | %P 285-309 | |
1648 | ||
1649 | %A R. D. Tennent | |
1650 | %T Mathematical semantics of Snobol 4 | |
1651 | %J Proc. ACM Symp. on Principles of Programming Languages | |
1652 | %D October 1973 | |
1653 | %P 95-107 | |
1654 | ||
1655 | %A R. D. Tennent | |
1656 | %T The denotational semantics of programming languages | |
1657 | %J Comm. Assoc. Comp. Mach. | |
1658 | %K acm cacm | |
1659 | %V 19 | |
1660 | %N 8 | |
1661 | %D August 1976 | |
1662 | %P 437-453 | |
1663 | ||
1664 | %A R. D. Tennent | |
1665 | %T Language design methods based on semantic principles | |
1666 | %J Acta Informatica | |
1667 | %V 8 | |
1668 | %D 1977 | |
1669 | %P 97-112 | |
1670 | ||
1671 | %A R. D. Tennent | |
1672 | %T A denotational definition of the programming language Pascal | |
1673 | %R Tech. Rep. 77-47 | |
1674 | %I Department of Computing and Information Science, Queen's University | |
1675 | %C Kingston, Ontario | |
1676 | %D July 1977 | |
1677 | ||
1678 | %A A. van Wijngaarden | |
1679 | %T Recursive definition of syntax and semantics | |
1680 | %E T. B. Steel, Jr. | |
1681 | %B Formal Language Description Languages for Computer Programming | |
1682 | %I North-Holland | |
1683 | %C Amsterdam | |
1684 | %D 1966 | |
1685 | %P 13-24 | |
1686 | ||
1687 | %A S. A. Walker | |
1688 | %A H. R. Strong, Jr. | |
1689 | %T Characterizations of flowchartable recursions | |
1690 | %J J. Comp. Sys. Sci. | |
1691 | %V 7 | |
1692 | %N 4 | |
1693 | %D August 1973 | |
1694 | %P 404-447 | |
1695 | ||
1696 | %A Mitchell Wand | |
1697 | %T A characterization of weakest preconditions | |
1698 | %J J. Comp. Sys. Sci. | |
1699 | %V 15 | |
1700 | %D 1977 | |
1701 | %P 209-212 | |
1702 | ||
1703 | %A Ben Wegbreit | |
1704 | %T Procedure closure in EL1 | |
1705 | %J Comp. J. | |
1706 | %V 17 | |
1707 | %N 1 | |
1708 | %D February 1974 | |
1709 | %P 38-43 | |
1710 | ||
1711 | %A Ben Wegbreit | |
1712 | %T The treatment of data types in EL1 | |
1713 | %J Comm. Assoc. Comp. Mach. | |
1714 | %K acm cacm | |
1715 | %V 17 | |
1716 | %N 5 | |
1717 | %D May 1974 | |
1718 | %P 251-264 | |
1719 | ||
1720 | %A Ben Wegbreit | |
1721 | %T Constructive methods in program verification | |
1722 | %J IEEE Trans. on Software Engineering | |
1723 | %V SE-3 | |
1724 | %N 3 | |
1725 | %D May 1977 | |
1726 | %P 193-209 | |
1727 | ||
1728 | %A W. A. Wulf | |
1729 | %A R. L. London | |
1730 | %A Mary Shaw | |
1731 | %T An introduction to the construction and verification of Alphard programs | |
1732 | %J IEEE Trans. on Software Engineering | |
1733 | %V SE-2 | |
1734 | %N 4 | |
1735 | %D December 1976 | |
1736 | %P 253-265 | |
1737 |