ゲーデル賞(Gödel Prize)論文及びGödel 論文を英語で読む（邪道）

Gödel Prize
https://sigact.org/prizes/gödel.html

20年以上前、Gödel の論文を読もうという身内の企画があった。計算機の仕事で時間が取れずに参加できなかった。
企画そのものが空中分解したのかもしれない。

読んでないという負い目をおいながら仕事をしてきた。
Gödel Prizeがあることを知った。

何一つ読んでいない。これらをすべて読みながら、Gödel の論文も読もうと思った。

Gödel, Kurt (1931), “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I.”, Monatshefte für Mathematik und Physik 38: 173–198, doi:10.1007/BF01700692.

英語じゃない。

Gödel, Kurt (1986), Feferman, Solomon, ed., Kurt Gödel: Collected Works: Volume I: Publications 1929-1936, Oxford University Press, pp. 144-195, ISBN 978-0-19-503964-1
Gödel, Kurt Meltzer, B.訳 (1992), On Formally

Undecidable Propositions of Principia Mathematica and Related Systems, Dover Books on Mathematics, Dover Publications, ISBN 978-0-486-66980-9

Gödel, Kurt; Hirzel, Martin (2000-11-27), “On formally undecidable propositions of Principia Mathematica and related systems I” (PDF), Boulder: 173-196
http://hirzels.com/martin/papers/canon00-goedel.pdf

Gödel, Kurt (2002), “Some metamathematical results on completeness and consistency, On formally undecidable propositions of Principia mathematica and related systems I, and On completeness and consistency”, in van Heijenoort, Jean, From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931, Source Books in the History of the Sciences (Fourth Printing ed.), Harvard University Press, pp. 592-617, ISBN 978-0-674-32449-7

Gödel, Kurt (2004), “On Formally Undecidable Propositions of the Principia Mathematica and Related Systems. I.”, in Davis, Martin, The Undecidable: Basic Papers on Undecidable Propositions, Unsolvable Problems and Computable Functions, Dover Books on Mathematics, Courier Corporation, pp. 4-38, ISBN 978-0-486-43228-1
https://books.google.co.jp/books?id=qW8x7sQ4JXgC&pg=PA4&redir_esc=y#v=onepage&q&f=false

英訳をまず確認中。

ゲーデル賞の方は、2013, 2014, 2015年の詳細記事がリンク切れになっていた。人名等を元に、論文を探して記録する。

http://citeseerx.ist.psu.edu/
https://arxiv.org
http://researchgate.net
で検索。

• Requested としたのはhttp://researchgate.net で関係者に著作物送達依頼した文献。

論文が揃ったら単語帳を作る予定。Wikipediaの記述も直接PDF等のURLを記載していないものもある。
該当する論文がWEBで無償では見当たらず、原型がArxivに掲載のあるものもある。論文URLの後ろに年号を記載した。
https://en.wikipedia.org/wiki/Gödel_Prize#cite_note-36
原文と同一のものはWikipediaに加筆する予定。

#人名一覧
2020: Robin A. Moser and Gábor Tardos
2019: Irit Dinur
2018: Oded Regev
2017: Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam Smith
2016: Stephen Brookes and Peter W. O’Hearn
2015: Daniel A. Spielman and Shang-Hua Teng
2014: Ronald Fagin, Amnon Lotem, and Moni Naor
2013: Antoine Joux, Dan Boneh, and Matthew K. Franklin
2012: Elias Koutsoupias, Christos H. Papadimitriou, Tim Roughgarden, Éva Tardos, Noam Nisan, and Amir Ronen
2011: Johan T. Håstad
2010: Sanjeev Arora and Joseph S. B. Mitchell
2009: Omer Reingold, Salil Vadhan, and Avi Wigderson
2008: Dan Spielman and Shang-Hua Teng
2007: Alexander A. Razborov and Steven Rudich
2006: Manindra Agrawal, Neeraj Kayal, and Nitin Saxena
2005: Noga Alon, Yossi Matias and Mario Szegedy
2004: Maurice Herlihy and Nir Shavit / Michael Saks and Fotios Zaharoglou
2003: Yoav Freund and Robert Schapire
2002: Géraud Sénizergues
2001: Sanjeev Arora, Uriel Feige, Shafi Goldwasser, Carsten Lund, László Lovász, Rajeev Motwani, Shmuel Safra, Madhu Sudan, and Mario Szegedy
2000: Moshe Vardi and Pierre Wolper
1999: Peter W. Shor
1998: Seinosuke Toda
1997: Joseph Halpern and Yoram Moses
1996: Mark Jerrum and Alistair Sinclair
1995: Neil Immerman and Róbert Szelepcsényi
1994: Johan Håstad
1993: László Babai, Shafi Goldwasser, Silvio Micali, Shlomo Moran, and Charles Rackoff

論文一覧

2020: Robin A. Moser and Gábor Tardos

The 2020 Gödel Prize is awarded to Robin A. Moser and Gábor Tardos for their algorithmic version of the Lovász Local Lemma in the paper:
“A constructive proof of the general Lovász Local Lemma,” Journal of the ACM 57(2): 11:1-11:15 (2010).
https://arxiv.org/pdf/0903.0544.pdf, 2009

References

[Knu69] Donald E. Knuth. The Art of Computer Programming, Vol. I, Addison Wesley, London, 1969, p. 396 (Exercise 11).
[EL75] Paul Erdo ̋s and La ́szl ́o Lov ́asz. Problems and results on 3-chromatic hypergraphs and some related ques- tions. In A. Hajnal, R. Rado and V.T. So ́s, editors, Infinite and Finite Sets (Colloq., Keszthely, 1973; dedicated to P. Erdo ̋s on his 60th birthday), volume II, pages 609–627. North-Holland, 1975.
[ES91] Paul Erdo ̋s and Joel Spencer. Lopsided Lova ́sz Local Lemma and Latin Transversals. Discrete Applied Mathematics, 30:151-154, 1991.
[Bec91] J ́oszef Beck. An Algorithmic Approach to the Lova ́sz Local Lemma. Random Structures and Algorithms, 2(4):343–365, 1991.
[Alo91] Noga Alon. A parallel algorithmic version of the local lemma. Random Structures and Algorithms, 2(4):367–378, 1991.
[KST93] JanKratochv ́ılandPetrSavicky ́andZsoltTuza.Onemoreoccurrenceofvariablesmakessatisfiability jump from trivial to NP-complete. SIAM J. Comput., Vol. 22, No. 1, pp. 203–210, 1993.
[MR98] Michael Molloy and Bruce Reed. Further Algorithmic Aspects of the Local Lemma. In Proceedings of the 30th Annual ACM Symposium on the Theory of Computing, pages 524–529, 1998.
[CS00] Artur Czumaj and Christian Scheideler. Coloring non-uniform hypergraphs: a new algorithmic approach to the general Lova ́sz local lemma. Symposium on Discrete Algorithms, 30–39, 2000.
[BKS03] Piotr Berman, Marek Karpinski, and Alexander D. Scott. Approximation hardness and satisfiability of bounded occurrence instances of SAT. Electronic Colloquium on Computational Complexity (ECCC), 10(022), 2003.
[Mos06] Robin A. Moser. On the Search for Solutions to Bounded Occurrence Instances of SAT. Not published. Semester Thesis, ETH Zu ̈rich. 2006.
[PT09] J ́anos Pach and G ́abor Tardos. Conflict-free colorings of graphs and hypergraphs. Manuscript, 2009.
[Sri08] Aravind Srinivasan. Improved algorithmic versions of the Lova ́sz Local Lemma. Proceedings of the nine- teenth annual ACM-SIAM symposium on Discrete algorithms (SODA), San Francisco, California, pp. 611–620, 2008.
[Wel08] Emo Welzl. Boolean Satisfiability - Combinatorics and Algorithms. Lecture notes, Version Fall 2008.
[Mos08] Robin A. Moser. Derandomizing the Lova ́sz Local Lemma more Effectively. Eprint, arXiv:0807.2120v2,
2008.
[Mos09] Robin A. Moser. A constructive proof of the Lova ́sz Local Lemma. Proceedings of the 41st annual ACM Symposium on Theory of Computing (STOC 2009), to appear. Available at arXiv:0810.4812v2, 2008.

####2019: Irit Dinur
https://sigact.org/prizes/gödel/citation2019.pdf

The 2019 Gödel Prize is awarded to Irit Dinur for her proof of the PCP Theorem in the paper:
The PCP theorem by gap amplification,
Journal of the ACM, Vol 54 (3), Article 12, 2007.
(preliminary version in the proceedings of the 38th Symposium on Theory of Computing, STOC 2006).
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=CC1C896ABF24E8D7EA957CD543AAACBB?doi=10.1.1.103.2644&rep=rep1&type=pdf

References

[1] S.Arora.Probabilisticcheckingofproofsandthehardnessofapproximationproblems.PhDthesis, U.C. Berkeley, 1994. Available via anonymous ftp as Princeton TR94-476.
[2] S. Arora, C. Lund, R. Motwani, M. Sudan, and M. Szegedy. Proof verification and intractability of approximation problems. J. ACM, 45(3):501–555, 1998.
[3] S. Arora and S. Safra. Probabilistic checking of proofs: A new characterization of NP. J. ACM, 45(1):70–122, 1998.
[4] L.Babai.Tradinggrouptheoryforrandomness.InProc.17thACMSymp.onTheoryofComputing, pages 421–429, 1985.
[5] L. Babai, L. Fortnow, and C. Lund. Non-deterministic exponential time has two-prover interactive protocols. Computational Complexity, 1:3–40, 1991.
[6] M. Ben-or, S. Goldwasser, J. Kilian, and A. Wigderson. Multi prover interactive proofs: How to remove intractability assumptions. In Proc. 20th ACM Symp. on Theory of Computing, pages 113–131, 1988.
[7] E. Ben-Sasson, O. Goldreich, P. Harsha, M. Sudan, and S. Vadhan. Robust PCPs of proximity, shorter PCPs and applications to coding. In Proc. 36th ACM Symp. on Theory of Computing, 2004.
[8] E. Ben-Sasson and M. Sudan. Robust locally testable codes and products of codes. In RANDOM: International Workshop on Randomization and Approximation Techniques in Computer Science, 2004.
[9] E. Ben-Sasson, M. Sudan, S. P. Vadhan, and A. Wigderson. Randomness-efficient low degree tests and short PCPs via epsilon-biased sets. In Proc. 35th ACM Symp. on Theory of Computing, pages 612–621, 2003.
[10] A. Bogdanov. Gap amplification fails below 1/2. Comment on ECCC TR05-046, can be found at http://eccc.uni-trier.de/eccc-reports/2005/TR05-046/commt01.pdf, 2005.
[11] I. Dinur and O. Reingold. Assignment testers: Towards combinatorial proofs of the PCP theorem. In Proceedings of the 45th Symposium on Foundations of Computer Science (FOCS), 2004.
[12] U. Feige, S. Goldwasser, L. Lova ́sz, S. Safra, and M. Szegedy. Approximating clique is almost NP-complete. Journal of the ACM, 43(2):268–292, 1996.
[13] U. Feige and J. Kilian. Impossibility results for recycling random bits in two-prover proof systems. In Proc. 27th ACM Symp. on Theory of Computing, pages 457–468, 1995.
[14] L. Fortnow, J. Rompel, and M. Sipser. On the power of multi-prover interactive protocols. Theo- retical Computer Science, 134(2):545–557, 1994.
35
[15] E. Friedgut, G. Kalai, and A. Naor. Boolean functions whose fourier transform is concentrated on the first two levels. Adv. in Applied Math., 29:427–437, 2002.
[16] O. Goldreich. A sample of samplers a computational perspective on sampling. Electronic Collo- quium on Computational Complexity TR97-020, 1997.
[17] O.GoldreichandS.Safra.AcombinatorialconsistencylemmawithapplicationtoprovingthePCP theorem. In RANDOM: International Workshop on Randomization and Approximation Techniques in Computer Science. LNCS, 1997.
[18] O. Goldreich and M. Sudan. Locally testable codes and PCPs of almost-linear length. In Proc. 43rd IEEE Symp. on Foundations of Computer Science, pages 13–22, 2002.
[19] O. Goldreich and A. Wigderson. Tiny families of functions with random properties: A qualitysize tradeoff for hashing. Journal of Random structures and Algorithms, 11(4):315–343, 1997.
[20] S. Goldwasser, S. Micali, and C. Rackoff. The knowledge complexity of interactive proofs. SIAM Journal on Computing, 18:186–208, 1989.
[21] P. Harsha and M. Sudan. Small PCPs with low query complexity. In STACS, pages 327–338, 2001.
[22] J. Ha ̊stad. Some optimal inapproximability results. Journal of ACM, 48:798–859, 2001.
[23] N. Linial and A. Wigderson. Expander graphs and their applications. Lecture notes of a course: http://www.math.ias.edu/ boaz/ExpanderCourse/, 2003.
[24] C. Lund, L. Fortnow, H. Karloff, and N. Nisan. Algebraic methods for interactive proof systems. Journal of the ACM, 39(4):859–868, October 1992.
[25] R. O’Donnell and V. Guruswami. Lecture notes from a course on: the PCP theorem and hardness of approximation. 2005.
[26] C. Papadimitriou and M. Yannakakis. Optimization, approximation and complexity classes. Jour- nal of Computer and System Sciences, 43:425–440, 1991.
[27] A. Polishchuk and D. Spielman. Nearly linear size holographic proofs. In Proc. 26th ACM Symp. on Theory of Computing, pages 194–203, 1994.
[28] J. Radhakrishnan. Private communication. 2005.
[29] R. Raz. A parallel repetition theorem. SIAM Journal on Computing, 27(3):763–803, June 1998.
[30] O. Reingold. Undirected st-connectivity in log-space. In Proc. 37th ACM Symp. on Theory of Computing, 2005.
[31] O. Reingold, S. Vadhan, and A. Wigderson. Entropy waves, the zig-zag graph product, and new constant-degree expanders and extractors. Annals of Mathematics, 155(1):157–187, 2002.
[32] A. Shamir. IP = PSPACE. Journal of the ACM, 39(4):869–877, October 1992. Prelim. version in 1990 FOCS, pages 11–15.
[33] M. Sipser and D. A. Spielman. Expander codes. IEEE Trans. Inform. Theory, 42(6, part 1):1710– 1722, 1996. Codes and complexity.

2018: Oded Regev

The 2018 Gödel Prize is awarded to Professor Oded Regev for his paper:
On lattices, learning with errors, random linear codes, and cryptography Journal of the ACM, volume 56, issue 6, 2009 (preliminary version in the 37th annual Symposium on Theory of Computing, STOC 2005.)
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.215.3543&rep=rep1&type=pdf

2017: Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam Smith

The 2017 Gödel Prize is awarded to Cynthia Dwork, Frank McSherry, Kobbi Nissim and Adam Smith for their work on Differential Privacy in the paper:
Calibrating Noise to Sensitivity in Private Data Analysis, Journal of Privacy and Confidentiality, Volume 7, Issue 3, 2016 (preliminary version in Theory of Cryptography, TCC 2006).
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=CC1C896ABF24E8D7EA957CD543AAACBB?doi=10.1.1.131.9267&rep=rep1&type=pdf
(Calibrating Data to Sensitivity in Private Data Analysis https://arxiv.org/pdf/1203.3453.pdf, 2014)

References

[1] N. R. Adam and J. C. Wortmann. Security-control methods for statistical data- bases: a comparative study. ACM Computing Surveys, 25(4), December 1989.
[2] Dakshi Agrawal and Charu C. Aggarwal. On the design and quantification of
privacy preserving data mining algorithms. In Proceedings of the Twentieth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Sys- tems. ACM, 2001.
[3] Rakesh Agrawal and Ramakrishnan Srikant. Privacy-preserving data mining. In Weidong Chen, Jeffrey F. Naughton, and Philip A. Bernstein, editors, SIGMOD Conference, pages 439–450. ACM, 2000.
[4] EliBen-Sasson,PrahladhHarsha,andSofyaRaskhodnikova.Some3cnfproperties are hard to test. In STOC, pages 345–354. ACM, 2003.
[5] Web page for the Bertinoro CS-Statistics workshop on privacy and confidentiality. Available from http://www.stat.cmu.edu/~hwainer, July 2005.
[6] Avrim Blum, Cynthia Dwork, Frank McSherry, and Kobbi Nissim. Practical privacy: The sulq framework. In PODS, 2005.
[7] Shuchi Chawla, Cynthia Dwork, Frank McSherry, Adam Smith, and Hoeteck Wee. Toward privacy in public databases. In Theory of Cryptography Confer- ence (TCC), pages 363–385, 2005.
[8] Shuchi Chawla, Cynthia Dwork, Frank McSherry, and Kunal Talwar. On the utility of privacy-preserving histograms. In 21st Conference on Uncertainty in Artificial Intelligence (UAI), 2005.
[9] Dorothy E. Denning. Secure statistical databases with random sample queries. ACM Transactions on Database Systems, 5(3):291–315, September 1980.
[10] Irit Dinur and Kobbi Nissim. Revealing information while preserving privacy. In
Proceedings of the Twenty-Second ACM SIGACT-SIGMOD-SIGART Symposium
on Principles of Database Systems, pages 202–210, 2003.
[11] Cynthia Dwork and Kobbi Nissim. Privacy-preserving datamining on vertically
partitioned databases. In Matthew K. Franklin, editor, CRYPTO, volume 3152
of Lecture Notes in Computer Science, pages 528–544. Springer, 2004.
[12] AlexandreV.Evfimievski,JohannesGehrke,andRamakrishnanSrikant.Limiting privacy breaches in privacy preserving data mining. In Proceedings of the Twenty- Second ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database
Systems, pages 211–222, 2003.
18 Cynthia Dwork, Frank McSherry, Kobbi Nissim, and Adam Smith
[13] Shafi Goldwasser and Silvio Micali. Probabilistic encryption. Journal of Computer and System Sciences, 28(2):270–299, April 1984.
[14] Gina Roque. Masking microdata with mixtures of normal distributions. University of California, Riverside, 2000. Doctoral Dissertation.
[15] Latanya Sweeney. k-anonymity: A model for protecting privacy. International Journal on Uncertainty, Fuzziness and Knowledge-based Systems, 10(5):557–570, 2002.

####2016: Stephen Brookes and Peter W. O’Hearn
https://eatcs.org/index.php/component/content/article/1-news/2280-2016-godel-prize

The 2016 Gödel Prize is awarded to Stephen Brookes and Peter W. O'Hearn for their invention of Concurrent Separation Logic, as described in the following two papers:
S. Brookes, A Semantics for Concurrent Separation Logic. Theoretical Computer Science 375(1-3): 227-270 (2007)
https://www.cs.cmu.edu/~brookes/papers/seplogicrevisedfinal.pdf

References

[1] G. Andrews. Concurrent Programming: Principles and Practice.
Benjamin/Cummings, 1991.
[2] L. Birkedal, N. Torp-Smith, and J.C. Reynolds. Local Reasoning about a Copying Garbage Collector. Proc. POPL Conference, Venice, pp. 220- 231, January 2004.
[3] R. Bornat, C. Calcagno, P. W. O’Hearn, and M. Parkinson. Permission accounting in separation logic. Proc. POPL 2005, pp. 59-70.
[4] R. Bornat, C. Calcagno, and P. W. O’Hearn. Local reasoning, separa- tion, and aliasing. Proc. 2nd ACM/SIGPLAN Workshop on Semantics, Program Analysis, and Computing Environments for Memory Manage- ment, SPACE 2004, January 2004.
[5] C. Boyapati, R. Lee, and M. Rinard. Ownership types for safe program- ming: Preventing data races and deadlocks. Proc. OOPSLA 2002: 211- 230, 2002.
[6] J. Boyland. Checking interference with fractional permissions. Proc. 10th Symposium on Static Analysis, R. Cousot, editor. Springer LNCS vol. 2694, pp. 55-72, 2003.
[7] P. Brinch Hansen. Structured multiprogramming. Comm. ACM, 15(7):574-578, July 1972.
[8] P. Brinch Hansen. Concurrent programming concepts. ACM Computing Surveys 5(4):223-245, December 1973.
[9] P. Brinch Hansen. Operating System Principles. Prentice Hall, 1973.
70
[10] P. Brinch Hansen. The programming language Concurrent Pascal. IEEE Trans. on Software Engr, SE-1(2):196-206. June 1975.
[11] S. Brookes. A semantics for concurrent separation logic. Invited paper, CONCUR 2004, London. August 2004. Springer LNCS 3170.
[12] S. Brookes, Traces, pomsets, fairness and full abstraction for communi- cating processes. Proc. CONCUR 2002, Brno. Springer LNCS vol. 2421, pp. 466-482. August 2002.
[13] S. Brookes. The essence of Parallel Algol. Proc. 11th Symposium on Logic in Computer Science, IEEE Computer Society Press (1996), pp. 164–173. Journal version: Inf. Comp. 179(1): 118-149, 2002.
[14] S. Brookes. Communicating Parallel Processes: Deconstructing CSP. In: Millenium Perspectives in Computer Science, Proc. 1999 Oxford- Microsoft Symposium in honour of Sir Tony Hoare. Palgrave, 2000.
[15] S. Brookes. Idealized CSP: Combining Procedures with Communicating Processes, 13th MFPS Conference, Pittsburgh, March 1997. Electronic Notes in Theoretical Computer Science 6, Elsevier, 1997.
[16] S. Brookes. Full abstraction for a shared-variable parallel language. Proc. 8th IEEE Symposium on Logic in Computer Science, IEEE Com- puter Society Press (1993), 98–109. Journal version in: Inf. Comp., vol 127(2):145-163, Academic Press, June 1996.
[17] S. Brookes and A.W. Roscoe. Deadlock Analysis in networks of commu- nicating processes. Distributed Computing 4:209-230, 1991.
[18] E. W. Dijkstra. Hierarchical ordering of sequential processes. Acta In- formatica, 1(2):115-138, 1972.
[19] E. W. Dijkstra. The structure of the “THE” multiprogramming system, Comm. ACM 11(5):341-346, May 1968.
[20] E. W. Dijkstra. Cooperating sequential processes. In: Programming Languages, F. Genuys (editor), pp. 43-112. Academic Press, 1968.
[21] C.A.R. Hoare. A structured paging system. Computer Journal 16(3):209- 215, 1973.
71

[22] C.A.R. Hoare. Parallel programming: an axiomatic approach. Computer Languages 1, 151-160, 1975.
[23] C.A.R. Hoare, Monitors: An operating system structuring concept, CACM 17(10): 549-557, October 1974.
[24] C.A.R. Hoare, Towards a Theory of Parallel Programming. In Oper- ating Systems Techniques, Hoare and Perrot, editors, pp. 61-71, Academic Press, 1972.
[25] S. Isthiaq and P. W. O’Hearn. BI as an assertion language for mutable data structures. Proc. 28th POPL conference, pp. 36-49, London, Jan- uary 2001.
[26] C.B. Jones. Development Methods for Computer Programs including a Notion of Interference. Ph.D. thesis, Oxford University, June 1981. Tech- nical Monograph PRG-25, Programming Reseacrh Group, Oxford Uni- versity Computing Laboratory.
[27] C.B. Jones. Specification and design of (parallel) programs. Proc. IFIP Conference, 1983.
[28] J. Misra and M. Chandy. Proofs of networks of processes. IEEE Trans- actions on Software Engineering, 7:417-426 (1981).
[29] H.C. Lauer. Correctness in operating systems. Ph. D. thesis, Carnegie Mellon University, 1973.
[30] P. W. O’Hearn. Notes on separation logic for shared-variable concur- rency. Unpublished manuscript, January 2002.
[31] P.W. O’Hearn. Resources, Concurrency, and Local Reasoning. Invited paper, CONCUR 2004, London, August 2004. Springer LNCS 3170. Complete paper in this volume.
[32] P.W. O’Hearn, H. Yang, and J.C. Reynolds. Separation and Information Hiding. Proc. 31st POPL conference, pp 268-280, Venice. ACM Press, January 2004.
[33] P.W. O’Hearn, J.C. Reynolds, and H. Yang. Local reasoning about pro- grams that alter data structures. Proc. 15th Conference of the European
72

Association for Computer Science Logic, Springer LNCS, vol. 2142, pp 1-19, 2001.
[34] P. W. O’Hearn and D. J. Pym. The logic of bunched implications. Bul- letin of Symbolic Logic, 5(2):215-244, June 1999.
[35] S. Owicki and L. Lamport, Proving liveness properties of concurrent programs, ACM TOPLAS, 4(3): 455-495, July 1982.
[36] S. Owicki and D. Gries. An axiomatic proof technique for parallel pro- grams I. Acta Informatica, 6:319-340, 1976.
[37] S. Owicki and D. Gries, Verifying properties of parallel programs: An axiomatic approach, Comm. ACM. 19(5):279-285, 1976.
[38] D. Park, On the semantics of fair parallelism. In: Abstract Software Specifications, Springer-Verlag LNCS vol. 86, 504–526, 1979.
[39] A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13(1):45-60, 1981.
[40] J. C. Reynolds. Intuitionistic reasoning about shared mutable data struc- ture. In J.Davies, A. W. Roscoe, and J. Woodcock, eds., Millenium per- spectives in computer science, pp. 303-321. Palgrave, 2000.
[41] J.C. Reynolds, Separation logic: a logic for shared mutable data struc- tures, Invited paper. Proc. 17th IEEE Conference on Logic in Computer Science, LICS 2002, pp. 55-74. IEEE Computer Society, 2002.
[42] J. C. Reynolds. Lecture notes on separation logic (15-819A3), chapter 8, page 178. Department of Computer Science, Carnegie-Mellon University, Spring 2003. Revised May 23, 2003.
[43] J. C. Reynolds, Towards a grainless semantics for shared-variable con- currency. Slides from Invited Lecture, 31st POPL concerence, Venice, January 2004.
[44] H. Yang. An example of local reasoning in BI pointer logic: The Schorr- Waite graph marking algorithm. Proc. SPACE 2001 Workshop on Se- mantics, Program Analysis and Computing Environments for Memory Management, pp. 41-68. IT University of Copenhagen, 2001.

P. W. O’Hearn, Resources, Concurrency, and Local Reasoning. Theoretical Computer Science 375(1-3): 271-307 (2007)
http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/concurrency.pdf

References

[1] G. Andrews. Concurrent programming: principles and practice. Benjamin/Cummings, 1991.
[2] A. Banerjee and D. A. Naumann. Representation independence, confinement and access con- trol. In 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2002.
[3] J. Berdine, C. Calcagno, and P. O’Hearn. A decidable fragment of separation logic. In Proceedings of FSTTCS, pages 97–109, 2004. LNCS 3328.
[4] R. Bornat. Variables as resource in Separation Logic. Proceedings of the 21st Conference on Mathematical Foundations of Computer Science, Springer LNCS, to appear, 2005.
[5] R. Bornat, C. Calcagno, P. O’Hearn, and M. Parkinson. Permission accounting in separation logic. In 32nd POPL, pages 59–70, 2005.
[6] C. Boyapati, R. Lee, and M. Rinard. Ownership types for safe programming: Preventing data races and deadlocks. OOPSLA, 2002.
[7] J. Boyland. Checking interference with fractional permissions. In R. Cousot, editor, Static Analysis: 10th International Symposium, volume 2694 of Lecture Notes in Computer Science, pages 55–72, Berlin, Heidelberg, New York, 2003. Springer.
[8] P. Brinch Hansen. The nucleus of a multiprogramming system. Comm. ACM, 13(4):238–250, 1970.
[9] P. Brinch Hansen. Structured multiprogramming. Comm. ACM, 15(7):574–578, 1972. Reprinted in [11].
[10] P. Brinch Hansen. Operating System Principles. Prentice Hall, 1973.
[11] P. Brinch Hansen, editor. The Origin of Concurrent Programming. Springer-Verlag, 2002.
[12] S. D. Brookes. A semantics for concurrent separation logic. Theoretical Computer Science, this Volume. Preliminary version appeared in Proceedings of the 15th CONCUR (2004), LNCS 3170, pp16-34., 2005.
[13] L. Caires. Behavioral and spatial observations in a logic for the pi-calculus. Proceedings of FOSSACS, LNCS 2987, 2004.
[14] L. Cardelli and L Caires. A spatial logic for concurrency. In 4th International Symposium on Theoretical Aspects of Computer Science, LNCS 2255:1–37, Springer, 2001.
[15] L. Cardelli and A. D. Gordon. Anytime, anywhere. Modal logics for mobile ambients. In 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 365–377, 2000.
[16] D. Clarke, J. Noble, and J. Potter. Simple ownership types for object containment. Proceedings of the 15th European Conference on Object-Oriented Programming, pages 53-76, Springer LNCS 2072, 2001.
[17] E. W. Dijkstra. Cooperating sequential processes. In F. Genuys, editor, Programming Lan- guages, pages 43–112. Academic Press, 1968. Reprinted in [11].
[18] E. W. Dijkstra. Hierarchical ordering of sequential processes. Acta Informatica, 1 2:115–138, October 1971. Reprinted in [11].
[19] J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.
[20] A. N. Habermann. Synchronization of communicating processes. Comm. ACM, 15(3):171–
176, 1972.
[21] T. Harris and K. Fraser. Language support for lightweight transactions. In Proceedings of
OOPSLA, pages 388–402, 2003.
[22] C. A. R. Hoare. Procedures and parameters: An axiomatic approach. In E. Engler, editor, Symposium on the Semantics of Algebraic Languages, pages 102–116. Springer, 1971. Lecture Notes in Math. 188.
[23] C. A. R. Hoare. Towards a theory of parallel programming. In Hoare and Perrot, editors, Operating Systems Techniques. Academic Press, 1972. Reprinted in [11].
[24] C. A. R. Hoare. Monitors: An operating system structuring concept. Comm. ACM, 17(10):549–557, 1974. Reprinted in [11].
[25] C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.
[26] C. B. Jones. Specification and design of (parallel) programs. IFIP Conference, 1983.
[27] C. B. Jones. Interference revisited. In J.E. Nicholls, editor, Proceedings of the 5th Annual Z User Meeting: Z User Workshop, Oxford, UK, pages 58–73, 1991. Springer-Verlag.
[28] C. B. Jones. Wanted: A compositional approach to concurrency. In A. McIver and C. Morgan, editors, Programming Methodology, pages 1–15, 2003. Springer-Verlag.
[29] H. T. Kung and P. L. Lehman. Concurrent manipulation of binary search trees. ACM Trans. Database Systems ,5, 354-382, 2005.
[30] M. Michael. Hazard pointers: Safe memory reclamation for lock-free objects. IEEE Trans. Parallel Distrib. Syst., 15(6):491–504, 2004.
[31] R. Milner. The polyadic pi-calculus: a tutorial. In F. L. Bauer, W. Brauer, and H. Schwicht- enberg, editors, Logic and Algebra of Specification, pages 203–246. Springer-Verlag, 1993.
[32] J. Misra and K.M. Chandy. Proofs of networks of processes. IEEE Trans. Software Eng., 7(4):417–426, 1981.
[33] D. A. Naumann and M. Barnett. Towards imperative modules: Reasoning about invariants and sharing of mutable state. Manuscript, 2 February, 2004.
[34] P. O’Hearn, J. Reynolds, and H. Yang. Local reasoning about programs that alter data struc- tures. In Proceedings of 15th Annual Conference of the European Association for Computer Science Logic, LNCS, pages 1–19. Springer-Verlag, 2001.
[35] P. W. O’Hearn and D. J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215–244, June 99.
[36] P. W. O’Hearn and R. D. Tennent, editors. Algol-like Languages. Two volumes, Birkhauser, Boston, 1997.
[37] P. W. O’Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. In 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 268– 280, Venice, January 2004.
[38] S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, (19):319–340, 1976.
[39] S. Owicki and D. Gries. Verifying properties of parallel programs: An axiomatic approach. Comm. ACM, 19(5):279–285, 1976.
[40] A. Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13(1), 45–60, 1981.
[41] D.J. Pym and C. Tofts. A calculus and logic of resources and processes. HP Labs Technical Report HPL-2004-170, 2004.
[42] J. C. Reynolds. Syntactic control of interference. In 5th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 39–46, Tucson, Arizona, January 1978. ACM, New York. Also in [36], vol 1.
[43] J. C. Reynolds. Separation logic: a logic for shared mutable data structures. Invited Paper, Proceedings of the 17th IEEE Symposium on Logic in Computer Science, pages 55-74, 2002.
[44] J. C. Reynolds. Shared variable concurrency. Chapter 6 of class notes from CS-819 C, CMU, 15 March, 2002.
[45] J. C. Reynolds. Towards a grainless semantics for shared variable concurrency. In Proceedings of FSTTCS, pages 35–48, 2004. LNCS 3328.
[46] F. Smith, D. Walker, and G. Morrisett. Alias types. Proceedings of ESOP’99.

2015: Daniel A. Spielman and Shang-Hua Teng

The 2015 Gödel Prize is awarded to Daniel A. Spielman and Shang-Hua Teng for their series of papers on nearly-linear-time Laplacian solvers:
Spectral sparsification of graphs. SIAM J. Computing 40:981-1025, 2011.
https://arxiv.org/pdf/0808.4134.pdf

References
[ACL06] Reid Andersen, Fan Chung, and Kevin Lang. Local graph partitioning using pager- ank vectors. Proceedings of the 47th Annual Symposium on Foundations of Computer Science, pages 475–486, 2006.
[AM01] Dimitris Achlioptas and Frank McSherry. Fast computation of low rank matrix approximations. In Proceedings of the 33rd Annual ACM Symposium on Theory of Computing, pages 611–618, 2001.
[AP09] Reid Andersen and Yuval Peres. Finding sparse cuts locally using evolving sets. In STOC ’09: Proceedings of the 41st annual ACM symposium on Theory of computing, pages 235–244, New York, NY, USA, 2009. ACM.
[Axe85] O. Axelsson. A survey of preconditioned iterative methods for linear systems of algebraic equations. BIT Numerical Mathematics, 25(1):165–187, March 1985.
[BGH+06] M. Bern, J. Gilbert, B. Hendrickson, N. Nguyen, and S. Toledo. Support-graph preconditioners. SIAM J. Matrix Anal. & Appl, 27(4):930–951, 2006.
[BH03] Erik G. Boman and Bruce Hendrickson. Support theory for preconditioning. SIAM Journal on Matrix Analysis and Applications, 25(3):694–717, 2003.
[BK96]
[Bol98] [BSS09]
[Che70] [Che89] [Chu97] [DR98] [DS91] [FK81] [GR01] [KMP10] [KVV04] [LPS88]
Andra ́s A. Benczu ́r and David R. Karger. Approximating s-t minimum cuts in O(n2) time. In Proceedings of The Twenty-Eighth Annual ACM Symposium On The Theory Of Computing (STOC ’96), pages 47–55, May 1996.
B ́ela Bollob ́as. Modern graph theory. Springer-Verlag, New York, 1998.
Joshua D. Batson, Daniel A. Spielman, and Nikhil Srivastava. Twice-Ramanujan sparsifiers. In Proceedings of the 41st Annual ACM Symposium on Theory of com- puting, pages 255–262, 2009.
J. Cheeger. A lower bound for smallest eigenvalue of laplacian. In Problems in Analysis, pages 195–199, In R.C. Gunning editor,, Princeton University Press, 1970.
Paul Chew. There are planar graphs almost as good as the complete graph. J. Comput. Syst. Sci., 39:205–219, 1989.
Fan R. K. Chung. Spectral Graph Theory. CBMS Regional Conference Series in Mathematics. American Mathematical Society, 1997.
Devdatt Dubhashi and Desh Ranjan. Balls and bins: a study in negative dependence. Random Structures and Algorithms, 13(2):99–124, 1998.
Persi Diaconis and Daniel Stroock. Geometric bounds for eigenvalues of markov chains. The Annals of Applied Probability, 1(1):36–61, 1991.
Z. Fu ̈redi and J. Komlo ́s. The eigenvalues of random symmetric matrices. Combi- natorica, 1(3):233–241, 1981.
Chris Godsil and Gordon Royle. Algebraic Graph Theory. Graduate Texts in Math- ematics. Springer, 2001.
Ioannis Koutis, Gary L. Miller, and Richard Peng. Approaching optimality for solving sdd systems. March 2010. Available at http://arxiv.org/abs/1003.2958v1.
Ravi Kannan, Santosh Vempala, and Adrian Vetta. On clusterings: Good, bad and spectral. J. ACM, 51(3):497–515, 2004.
A. Lubotzky, R. Phillips, and P. Sarnak. Ramanujan graphs. Combinatorica, 8(3):261–277, 1988.
[Mar88] G. A. Margulis. Explicit group theoretical constructions of combinatorial schemes and their application to the design of expanders and concentrators. Problems of Information Transmission, 24(1):39–46, July 1988.
[Moh91] Bojan Mohar. The Laplacian spectrum of graphs. In Graph Theory, Combinatorics, and Applications, pages 871–898. Wiley, 1991.
[Rag88] Prabhakar Raghavan. Probabilistic construction of deterministic algorithms: Ap- proximating packing integer programs. J. Comput. Syst. Sci., 37:130–143, 1988.
[SJ89] Alistair Sinclair and Mark Jerrum. Approximate counting, uniform generation and rapidly mixing Markov chains. Information and Computation, 82(1):93–133, July 1989.
[SS08] Daniel A. Spielman and Nikhil Srivastava. Graph sparsification by effective resis- tances. In Proceedings of the 40th annual ACM Symposium on Theory of Computing, pages 563–568, 2008.
[ST04] Daniel A. Spielman and Shang-Hua Teng. Nearly-linear time algorithms for graph partitioning, graph sparsification, and solving linear systems. In Proceedings of the thirty-sixth annual ACM Symposium on Theory of Computing, pages 81–90, 2004. Full version available at http://arxiv.org/abs/cs.DS/0310051.
[ST08a] Daniel A. Spielman and Shang-Hua Teng. A local clustering algorithm for mas- sive graphs and its application to nearly-linear time graph partitioning. CoRR, abs/0809.3232, 2008. Available at http://arxiv.org/abs/0809.3232. Submitted to SICOMP.
[ST08b] Daniel A. Spielman and Shang-Hua Teng. Nearly-linear time algorithms for pre- conditioning and solving symmetric, diagonally dominant linear systems. CoRR, abs/cs/0607105, 2008. Available at http://www.arxiv.org/abs/cs.NA/0607105. Submitted to SIMAX.
[Tar75] R. E. Tarjan. Efficiency of a good but not linear set union algorithm. Journal of the ACM, 22(2):448–501, 1975.
[TB97] L. N. Trefethen and D. Bau. Numerical Linear Algebra. SIAM, Philadelphia, PA, 1997.
[Tre05] Lucan Trevisan. Approximation algorithms for unique games. Proceedings of the 46th Annual IEEE Symposium on Foundations of Computer Science, pages 197–205, Oct. 2005.
[Vu07] Van Vu. Spectral norm of random matrices. Combinatorica, 27(6):721–736, 2007.

A local clustering algorithm for massive graphs and its application to nearly linear time
graph partitioning. SIAM J. Computing 42:1-26, 2013.
https://arxiv.org/pdf/0809.3232.pdf

References

[ABC+ 07] Reid Andersen, Christian Borgs, Jennifer T. Chayes, John E. Hopcraft, Vahab S. Mirrokni, and Shang-Hua Teng. Local computation of pagerank contributions. In Anthony Bonato and Fan R. K. Chung, editors, WAW, volume 4863 of Lecture Notes in Computer Science, pages 150–165. Springer, 2007.
[ACL06] Reid Andersen, Fan Chung, and Kevin Lang. Local graph partitioning using pager- ank vectors. Proceedings: 47th Annual Symposium on Foundations of Computer Science, pages 475–486, 2006.
[ACL07] Reid Andersen, Fan R. K. Chung, and Kevin J. Lang. Local partitioning for directed graphs using pagerank. In Anthony Bonato and Fan R. K. Chung, editors, WAW, volume 4863 of Lecture Notes in Computer Science, pages 166–178. Springer, 2007.
[AHK04] Sanjeev Arora, Elad Hazan, and Satyen Kale. 0(sqrt (log n)) approximation to Sparsest Cut in ̃o(n2) time. In FOCS: IEEE Symposium on Foundations of Com- puter Science (FOCS), pages 238–247, 2004.
[AK07] Sanjeev Arora and Satyen Kale. A combinatorial, primal-dual approach to semidef- inite programs. In STOC ’07: Proceedings of the thirty-ninth annual ACM sympo- sium on Theory of computing, pages 227–236, New York, NY, USA, 2007. ACM.
[And08] Reid Andersen. A local algorithm for finding dense subgraphs. In Proceedings of the Nineteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2008, San Francisco, California, USA, January 20-22, 2008, pages 1003–1009. SIAM, 2008.
[ARV04] Sanjeev Arora, Satish Rao, and Umesh Vazirani. Expander flows, geometric embed- dings and graph partitioning. In STOC ’04: Proceedings of the thirty-sixth annual ACM symposium on Theory of computing, pages 222–231, New York, NY, USA, 2004. ACM.
[Cor05] Intel Corporation. Morre’s law. ftp://download.intel.com/museum/Moores Law/Printed Mater 2005.
[GS05] A. Gulli and A. Signorini. The indexable web is more than 11.5 billion pages. In
WWW ’05: Special interest tracks and posters of the 14th international conference on World Wide Web, pages 902–903. ACM, 2005.
[KRV06] Rohit Khandekar, Satish Rao, and Umesh Vazirani. Graph partitioning using sin- gle commodity flows. In STOC ’06: Proceedings of the thirty-eighth annual ACM symposium on Theory of computing, pages 385–390, New York, NY, USA, 2006. ACM.
[KVV04] Ravi Kannan, Santosh Vempala, and Adrian Vetta. On clusterings: Good, bad and spectral. J. ACM, 51(3):497–515, 2004.
[LH08] Jure Leskovec and Eric Horvitz. Planetary-scale views on a large instant-messaging network. In WWW ’08: Proceeding of the 17th international conference on World Wide Web, pages 915–924. ACM, 2008.
[LR99] Tom Leighton and Satish Rao. Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms. Journal of the ACM, 46(6):787– 832, November 1999.
[LS90] L. Lovasz and M. Simonovits. The mixing rate of Markov chains, an isoperimetric inequality, and computing the volume. In IEEE, editor, Proceedings: 31st Annual Symposium on Foundations of Computer Science: October 22–24, 1990, St. Louis, Missouri, volume 1, pages 346–354, 1109 Spring Street, Suite 300, Silver Spring, MD 20910, USA, 1990. IEEE Computer Society Press.
[LS93] Lovasz and Simonovits. Random walks in a convex body and an improved volume algorithm. RSA: Random Structures & Algorithms, 4:359–412, 1993.
[OSVV08] Lorenzo Orecchia, Leonard J. Schulman, Umesh V. Vazirani, and Nisheeth K. Vish- noi. On partitioning graphs via single commodity flows. In STOC ’08: Proceedings of the 40th annual ACM symposium on Theory of computing, pages 461–470, New York, NY, USA, 2008. ACM.
[PBMW98] Lawrence Page, Sergey Brin, Rajeev Motwani, and Terry Winograd. The pagerank citation ranking: Bringing order to the web. Technical report, Stanford Digital
Library Technologies Project, Stanford University, Stanford, CA, USA, November 1998.
[SLM+ 02] Ashish Sharma, Xinlian Liu, Paul Miller, Aiichiro Nakano, Rajiv K. Kalia, Priya Vashishta, Wei Zhao, Timothy J. Campbell, and Andy Haas. Immersive and in- teractive exploration of billion-atom systems. In VR ’02: Proceedings of the IEEE Virtual Reality Conference 2002, page 217. IEEE Computer Society, 2002.
[SS06] Jir ́ı S ́ıma and Satu Elisa Schaeffer. On the NP-completeness of some graph cluster measures. In Jir ́ı Wiedermann, Gerard Tel, Jaroslav Pokorny ́, M ́aria Bielikov ́a, and Julius Stuller, editors, SOFSEM, volume 3831 of Lecture Notes in Computer Science, pages 530–537. Springer, 2006.
[ST03] Daniel A. Spielman and Shang-Hua Teng. Nearly-linear time algorithms for graph partitioning, graph sparsification, and solving linear systems. available at http://arxiv.org/abs/cs.DS/0310051. An extended abstract appeared in Pro- ceedings of the thirty-sixth annual ACM symposium on Theory of computing, 81–90, 2003.
[ST08a] Daniel A. Spielman and Shang-Hua Teng. Nearly-linear time algorithms for pre- conditioning and solving symmetric, diagonally dominant linear systems. CoRR, abs/cs/0607105, 2008. Available at http://www.arxiv.org/abs/cs.NA/0607105.
[ST08b] Daniel A. Spielman and Shang-Hua Teng. Spectral sparsification of graphs. CoRR, abs/0808.4134, 2008. Available at http://arxiv.org/abs/0808.4134.

Nearly linear time algorithms for preconditioning and solving symmetric, diagonally dominant linear systems. SIAM J. Matrix Anal. Appl. 35:835-885, 2014.
https://arxiv.org/pdf/cs/0607105.pdf

References

[ABN08] I. Abraham, Y. Bartal, and O. Neiman. Nearly tight low stretch spanning trees. In Proceedings of the 49th Annual IEEE Symposium on Foundations of Computer Science, pages 781–790, Oct. 2008.
[AKPW95] Noga Alon, Richard M. Karp, David Peleg, and Douglas West. A graph-theoretic game and its application to the k-server problem. SIAM Journal on Computing, 24(1):78–100, February 1995.
[AM85] [AN12]
[Axe85] [BCHT04]
[BCPT05]
[BGH+06] [BH01] [BH03a]
William N. Anderson and Thomas D. Morley. Eigenvalues of the laplacian of a graph. Linear and Multilinear Algebra, 18(2):141–145, 1985.
Ittai Abraham and Ofer Neiman. Using petal-decompositions to build a low stretch spanning tree. In Proceedings of the 44th Annual ACM Symposium on the Theory of Computing (STOC ’12), pages 395–406, 2012.
O. Axelsson. A survey of preconditioned iterative methods for linear systems of algebraic equations. BIT Numerical Mathematics, 25(1):165–187, March 1985.
Erik G. Boman, Doron Chen, Bruce Hendrickson, and Sivan Toledo. Maximum- weight-basis preconditioners. Numerical linear algebra with applications, 11(8– 9):695–721, October/November 2004.
Erik G. Boman, Doron Chen, Ojas Parekh, and Sivan Toledo. On factor width and symmetric h-matrices. Linear Algebra and its Applications, 405(1):239–248, August 2005.
M. Bern, J. Gilbert, B. Hendrickson, N. Nguyen, and S. Toledo. Support-graph preconditioners. SIAM J. Matrix Anal. & Appl, 27(4):930–951, 2006.
Erik Boman and B. Hendrickson. On spanning tree preconditioners. Manuscript, Sandia National Lab., 2001.
Mario Bebendorf and Wolfgang Hackbusch. Existence of H-matrix approximants to the inverse FE-matrix of elliptic operators with L∞-coefficients. Numerische Mathematik, 95(1):1–28, July 2003.
[BH03b]
[BHM01] W. L. Briggs, V. E. Henson, and S. F. McCormick. A Multigrid Tutorial, 2nd
Erik G. Boman and Bruce Hendrickson. Support theory for preconditioning. SIAM Journal on Matrix Analysis and Applications, 25(3):694–717, 2003.
Edition. SIAM, 2001.
[BHV08] Erik G. Boman, Bruce Hendrickson, and Stephen A. Vavasis. Solving elliptic finite element systems in near-linear time with support preconditioners. SIAM J. on Numerical Analysis, 46(6):3264–3284, 2008.
[BMN04] M. Belkin, I. Matveeva, and P. Niyogi. Regularization and semi-supervised learning on large graphs. Proc. 17th Conf. on Learning Theory, pages 624–638, 2004.
[BSS09]
[CKM+11]
[CT03] [CW82] [Dem89] [DER86] [DS07] [DS08]
[EEST08] [FG04] [Fie73] [Geo73] [GMZ95]
[GO88]
Joshua D. Batson, Daniel A. Spielman, and Nikhil Srivastava. Twice-Ramanujan sparsifiers. In Proceedings of the 41st Annual ACM Symposium on Theory of com- puting, pages 255–262, 2009.
Paul Christiano, Jonathan A. Kelner, Aleksander Madry, Daniel A. Spielman, and Shang-Hua Teng. Electrical flows, laplacian systems, and faster approximation of maximum flow in undirected graphs. In Proceedings of the 43rd annual ACM sym- posium on Theory of computing, STOC ’11, pages 273–282, New York, NY, USA, 2011. ACM.
Doron Chen and Sivan Toledo. Vaidya’s preconditioners: implementation and ex- perimental study. Electronic Transactions on Numerical Analysis, 16:30–49, 2003.
D. Coppersmith and S. Winograd. On the asymptotic complexity of matrix multi- plication. SIAM Journal on Computing, 11(3):472–492, August 1982.
James Demmel. On floating point errors in cholesky. Technical report, Courant Institute, 1989. LAPACK Working Note 14.
I. S. Duff, A. M. Erisman, and J. K. Reid. Direct Methods for Sparse Matrices. Oxford Science Publications, 1986.
Samuel I. Daitch and Daniel A. Spielman. Support-graph preconditioners for 2- dimensional trusses. CoRR, abs/cs/0703119, 2007.
Samuel I. Daitch and Daniel A. Spielman. Faster approximate lossy generalized flow via interior point algorithms. In Proceedings of the 40th Annual ACM Symposium on Theory of Computing, pages 451–460, 2008.
Michael Elkin, Yuval Emek, Daniel A. Spielman, and Shang-Hua Teng. Lower- stretch spanning trees. SIAM Journal on Computing, 32(2):608–628, 2008.
A. Frangioni and C. Gentile. New preconditioners for KKT systems of network flow problems. SIAM Journal on Optimization, 14(3):894–913, 2004.
Miroslav Fiedler. Algebraic connectivity of graphs. Czechoslovak Mathematical Journal, 23(98):298–305, 1973.
J. A. George. Nested dissection of a regular finite element mesh. SIAM J. Numer. Anal., 10:345–363, 1973.
Keith D. Gremban, Gary L. Miller, and Marco Zagha. Performance evaluation of a new parallel preconditioner. In Proceedings of the 9th International Symposium on Parallel Processing, pages 65–69. IEEE Computer Society, 1995.
G. H. Golub and M. Overton. The convergence of inexact Chebychev and Richardson iterative methods for solving linear systems. Numerische Mathematik, 53:571–594, 1988.
[Gre96]
[GT87] [GV61]
[Har72] [Hig02]
[Jor69] [Jos97] [KM07]
[KM10]
[KMP10]
[KMP11]
[KMP12]
[KMST10]
[LRT79]
Keith Gremban. Combinatorial Preconditioners for Sparse, Symmetric, Diagonally Dominant Linear Systems. PhD thesis, Carnegie Mellon University, CMU-CS-96- 123, 1996.
John R. Gilbert and Robert Endre Tarjan. The analysis of a nested dissection algorithm. Numerische Mathematik, 50(4):377–404, February 1987.
Gene H. Golub and Richard S. Varga. Chebyshev semi-iterative methods, successive overrelaxation iterative methods, and second order richardson iterative methods. Numerische Mathematik, 3:157–168, 1961. 10.1007/BF01386014.
Frank Harary. Graph Theory. Addison-Wesley, 1972.
Nicholas J. Higham. Accuracy and Stability of Numerical Algorithms. Society for
Industrial and Applied Mathematics, Philadelphia, PA, USA, second edition, 2002. Camille Jordan. Sur les assemblages de lignes. Journal fu ̈r die reine und angewandte
Mathematik, 70:185–190, 1869.
Anil Joshi. Topics in Optimization and Sparse Linear Systems. PhD thesis, UIUC,
1997.
Ioannis Koutis and Gary L. Miller. A linear work, o(n1/6) time, parallel algorithm for solving planar Laplacians. In Proceedings of the 18th Annual ACM-SIAM Sym- posium on Discrete Algorithms, pages 1002–1011, 2007.
J.A. Kelner and A. Madry. Faster generation of random spanning trees. In Foun- dations of Computer Science, 2009. FOCS’09. 50th Annual IEEE Symposium on, pages 13–21. IEEE, 2010. This result was substantially improved as a result of an observation by James Propp. He will be added as a coauthor on the journal version.
I. Koutis, G.L. Miller, and R. Peng. Approaching optimality for solving sdd linear systems. In Foundations of Computer Science (FOCS), 2010 51st Annual IEEE Symposium on, pages 235 –244, 2010.
I. Koutis, G.L. Miller, and R. Peng. A nearly-mlogn time solver for sdd linear systems. In Foundations of Computer Science (FOCS), 2011 52nd Annual IEEE Symposium on, pages 590–598, 2011.
Jonathan A. Kelner, Gary L. Miller, and Richard Peng. Faster approximate mul- ticommodity flow using quadratically coupled flows. In Proceedings of the 44th symposium on Theory of Computing, STOC ’12, pages 1–18, New York, NY, USA, 2012. ACM.
Alexandra Kolla, Yury Makarychev, Amin Saberi, and Shang-Hua Teng. Subgraph sparsification and nearly optimal ultrasparsifiers. In Proceedings of the 42nd ACM symposium on Theory of computing, STOC ’10, pages 57–66, 2010.
Richard J. Lipton, Donald J. Rose, and Robert Endre Tarjan. Generalized nested dissection. SIAM Journal on Numerical Analysis, 16(2):346–358, April 1979.
[Mal00] A. N. Malyshev. A note on the stablity of gauss-jordan elimination for diagonally dominant matrices. Computing, 65:281–284, 2000.
[Mih89] Milena Mihail. Conductance and convergence of Markov chains—A combinatorial treatment of expanders. In 30th Annual IEEE Symposium on Foundations of Com- puter Science, pages 526–531, 1989.
[MMP+05] Bruce M. Maggs, Gary L. Miller, Ojas Parekh, R. Ravi, and Shan Leung Maverick Woo. Finding effective support-tree preconditioners. In Proceedings of the seven- teenth annual ACM symposium on Parallelism in algorithms and architectures, pages 176–185, 2005.
[Rei98] John Reif. Efficient approximate solution of sparse linear systems. Computers and Mathematics with Applications, 36(9):37–58, 1998.
[Sot10] Andrew Sothers. On the complexity of matrix multiplication. PhD thesis, University of Edinburg, 2010.
[SS08] Daniel A. Spielman and Nikhil Srivastava. Graph sparsification by effective resis- tances. In Proceedings of the 40th annual ACM Symposium on Theory of Computing, pages 563–568, 2008.
[SST06] Arvind Sankar, Daniel A. Spielman, and Shang-Hua Teng. Smoothed analysis of the condition numbers and growth factors of matrices. SIAM Journal on Matrix Analysis and Applications, 28(2):446–476, 2006.
[ST] Daniel A. Spielman and Shang-Hua Teng. A local clustering algorithm for massive graphs and its application to nearly-linear time graph partitioning. SIAM Journal on Computing. To appear.
[ST04] Daniel A. Spielman and Shang-Hua Teng. Nearly-linear time algorithms for graph partitioning, graph sparsification, and solving linear systems. In Proceedings of the thirty-sixth annual ACM Symposium on Theory of Computing, pages 81–90, 2004. Full version available at http://arxiv.org/abs/cs.DS/0310051.
[ST08] Gil Shklarski and Sivan Toledo. Rigidity in finite-element matrices: Sufficient con- ditions for the rigidity of structures and substructures. SIAM Journal on Matrix Analysis and Applications, 30(1):7–40, 2008.
[ST11] Daniel A. Spielman and Shang-Hua Teng. Spectral sparsification of graphs. SIAM Journal on Computing, 40(4):981–1025, 2011.
[Str86] Gilbert Strang. Introduction to Applied Mathematics. Wellesley-Cambridge Press, 1986.
[SW09] Daniel A. Spielman and Jaeoh Woo. A note on preconditioning by low-stretch spanning trees. CoRR, abs/0903.2816, 2009. Available at http://arxiv.org/abs/0903.2816.
[TB97] [Vai90]
[Wil12]
[ZBL+ 03]
[ZGL03]
[Zha05]
L. N. Trefethen and D. Bau. Numerical Linear Algebra. SIAM, Philadelphia, PA, 1997.
Pravin M. Vaidya. Solving linear equations with symmetric diagonally dominant matrices by constructing good preconditioners. Unpublished manuscript UIUC 1990. A talk based on the manuscript was presented at the IMA Workshop on Graph Theory and Sparse Matrix Computation, October 1991, Minneapolis., 1990.
V. Vassilevska Williams. Multiplying matrices faster than coppersmith-winograd. In Proceedings of the 44th Annual ACM Symposium on the Theory of Computing (STOC ’12), pages 887–898, 2012.
Dengyong Zhou, Olivier Bousquet, Thomas Navin Lal, Jason Weston, and Bernhard Scho ̈lkopf. Learning with local and global consistency. In Adv. in Neural Inf. Proc. Sys. 16, pages 321–328, 2003.
Xiaojin Zhu, Zoubin Ghahramani, and John D. Lafferty. Semi-supervised learning using Gaussian fields and harmonic functions. In Proc. 20th Int. Conf. on Mach. Learn., 2003.
Fuzhen Zhang, editor. The Schur Complement and its Applications, volume 4 of Numerical Methods and Algorithms. Springer, 2005.

####2014: Ronald Fagin, Amnon Lotem, and Moni Naor
Optimal Aggregation Algorithms for Middleware
https://arxiv.org/pdf/cs/0204046.pdf

####2013: Antoine Joux, Dan Boneh, and Matthew K. Franklin
A One Round Protocol for Tripartite Diffie–Hellman
Antoine Joux, Journal of Cryptology volume 17, pages263–276(2004)
https://link.springer.com/content/pdf/10.1007/s00145-004-0312-y.pdf

Identity-Based Encryption from the Weil Pairing
Dan Boneh∗ Matthew Franklin
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.66.1131&rep=rep1&type=pdf

Nisan, Noam; Ronen, Amir (2001). "Algorithmic Mechanism Design". Games and Economic Behavior. 35 (1–2): 166–196.
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.21.1731&rep=rep1&type=pdf

####2012: Elias Koutsoupias, Christos H.Papadimitriou, Tim Roughgarden, Éva Tardos, Noam Nisan, and Amir Ronen

Koutsoupias, Elias; Papadimitriou, Christos (2009). "Worst-case equilibria". Computer Science Review. 3 (2): 65–69. doi:10.1016/j.cosrev.2009.04.003.
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=08343A18C75A6F5A0E57B25562499E5C?doi=10.1.1.102.6991&rep=rep1&type=pdf

Roughgarden, Tim; Tardos, Éva (2002). "How bad is selfish routing?". Journal of the ACM. 49 (2): 236–259. CiteSeerX 10.1.1.147.1081. doi:10.1145/506147.506153.
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.147.1081&rep=rep1&type=pdf

Nisan, Noam; Ronen, Amir (2001). "Algorithmic Mechanism Design". Games and Economic Behavior. 35 (1–2): 166–196. CiteSeerX 10.1.1.21.1731. doi:10.1006/game.1999.0790.
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.21.1731&rep=rep1&type=pdf

####2011: Johan T. Håstad
https://sigact.org/prizes/gödel/2011.html

The 2011 Gödel Prize is awarded to Johan T. Håstad for his paper:
Some optimal inapproximability results, Journal of the ACM, 48: 798--859, 2001.
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.638.2808&rep=rep1&type=pdf

####2010: Sanjeev Arora and Joseph S. B. Mitchell
https://sigact.org/prizes/gödel/2010.html

The 2010 Gödel Prize is awarded to
Sanjeev Arora and Joseph S.B. Mitchell for their concurrent discovery of a polynomial-time approximation scheme (PTAS) for the Euclidean Travelling Salesman Problem (ETSP):
Sanjeev Arora. (1998). Polynomial-time approximation schemes for Euclidean TSP and other geometric problems, Journal ACM 45(5), 753-782.
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.23.6765&rep=rep1&type=pdf
Joseph S.B. Mitchell (1999). Guillotine subdivisions approximate polygonal subdivisions: A simple polynomial-time approximation scheme for geometric TSP, k-MST, and related problems, SIAM J. Computing 28(4), 1298-1309.
http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=EBC1BCCD86A8ECD59B018C11236ECA89?doi=10.1.1.56.4805&rep=rep1&type=pdf

####2009: Omer Reingold, Salil Vadhan, and Avi Wigderson
https://sigact.org/prizes/gödel/2009.html

The 2009 Gödel Prize for outstanding papers in the area of theoretical computer science is awarded to
(1) Entropy waves, the zig-zag graph product and new constant degree expanders. Omer Reingold, Salil Vadhan and Avi Wigderson, Annals of Mathematics, Vol 155, (2002), 157-187
https://arxiv.org/pdf/math/0406038.pdf
and
(2) Undirected connectivity in Log-Space. Omer Reingold, Journal of ACM, Vol 55 (4) (2007).

• Requested.

####2008: Dan Spielman and Shang-Hua Teng
https://sigact.org/prizes/gödel/2008.html

The 2008 Gödel Prize for outstanding papers in the area of theoretical computer science is awarded to
Daniel A. Spielman and Shang-Hua Teng for their paper: Smoothed analysis of algorithms: Why the simplex algorithm usually takes polynomial time by Daniel A. Spielman and Shang-Hua Teng, Journal of the ACM (JACM), 51(3), May 2004, 385-463.
First presented at the Annual ACM Symposium on the Theory of Computing (STOC 01), 2001, 296-305.
https://arxiv.org/pdf/math/0212413.pdf

####2007: Alexander A. Razborov and Steven Rudich
https://sigact.org/prizes/gödel/2007.html

The 2007 Gödel Prize for outstanding papers in the area of theoretical computer science is awarded to Alexander A. Razborov and Steven Rudich for their paper:
Natural Proofs, Journal of Computer and System Sciences, Vol. 55, No. 1, 1997, pp. 24-35.
First presented at the Twenty-sixth Annual ACM Symposium on Theory of computing, Montreal, Quebec, Canada. 1994, pp. 204-213.
https://reader.elsevier.com/reader/sd/pii/S002200009791494X?token=9E8D5C0FAA5F8E450DFB32BDEDED9B07CACDC4BD40EA21B35A33BF9E74A24E840B6AF2E6FF1C20F6ED02778CA1FC109C
####2006: Manindra Agrawal, Neeraj Kayal, and Nitin Saxena
https://sigact.org/prizes/gödel/2006.html
The 2006 Gödel Prize for outstanding papers in the area of theoretical computer science is awarded to Manindra Agrawal, Neeraj Kayal, and Nitin Saxena for their paper:
PRIMES is in P. Annals of Mathematics 160(2), 781-793, 2004.
https://web.archive.org/web/20110607101302/http://math.berkeley.edu/~coleman/Courses/Fall08/Cryptography/primality_v6.pdf

2005: Noga Alon, Yossi Matias and Mario Szegedy

The 2005 Gödel Prize for outstanding papers in the area of theoretical computer science is awarded to
Noga Alon, Yossi Matias and Mario Szegedy for their paper: The space complexity of approximating the frequency moments. Journal of Computer and System Sciences 58 (1999), 137-147 First presented at the 28th ACM Symposium on Theory of Computing, 1996.
http://www.math.tau.ac.il/~nogaa/PDFS/amsz4.pdf

2004: Maurice Herlihy and Nir Shavit / Michael Saks and Fotios Zaharoglou

The 2004 Gödel Prize for outstanding journal articles in theoretical computer science is shared between the papers:
"The Topological Structure of Asynchronous Computation" by Maurice Herlihy and Nir Shavit, Journal of the ACM, Vol. 46 (1999), 858-923,
http://cs.brown.edu/~mph/HerlihyS99/p858-herlihy.pdf
and
"Wait-Free k-Set Agreement Is Impossible: The Topology of Public Knowledge" by Michael Saks and Fotios Zaharoglou, SIAM J. on Computing, Vol. 29 (2000), 1449-1483.

• Requested.

2003: Yoav Freund and Robert Schapire

The prize was awarded to
Yoav Freund and Robert Schapire for their paper "A Decision Theoretic Generalization of On-Line Learning and an Application to Boosting," Journal of Computer and System Sciences 55 (1997), pp. 119-139.
https://www-ai.cs.tu-dortmund.de/LEHRE/PG/PG445/literatur/freund_schapire_97a.pdf

2002: Géraud Sénizergues

Geraud Senizergues, for "L(A)=L(B)? Decidability results from complete formal systems", Theoretical Computer Science 251 (2001), pp.1-166.
https://reader.elsevier.com/reader/sd/pii/S0304397500002851?token=64A2B37155D426438B12D3E16D9DA7D657C01E4E4944CA307F3319EB3724727119FF108137109C77E438B12E754C1179

2001: Sanjeev Arora, Uriel Feige, Shafi Goldwasser, Carsten Lund, László Lovász, Rajeev Motwani, Shmuel Safra, Madhu Sudan, and Mario Szegedy

The 2001 Gödel Prize for outstanding journal article in the area of theoretical computer science is awarded to
Sanjeev Arora, Uriel Feige, Shafi Goldwasser, Carsten Lund, Laszlo Lovász, R. Motwani, Shmuel Safra, Madhu Sudan, and Mario Szegedy for the following series of papers:
"Interactive Proofs and the Hardness of Approximating Cliques". Uriel Feige, Shafi Goldwasser, Laszlo Lovász, Shmuel Safra, and Mario Szegedy. Journal of the ACM 43 (1996), 268-292.
https://www.researchgate.net/profile/Mario_Szegedy/publication/234783217_Interactive_proofs_and_the_hardness_of_approximating_cliques/links/09e41514878e8c2f78000000/Interactive-proofs-and-the-hardness-of-approximating-cliques.pdf
"Probabilistic Checking of Proofs: A New Characterization of NP". Sanjeev Arora and Shmuel Safra. Journal of the ACM 45 (1998), 70-122.
https://web.archive.org/web/20110610101051/http://www.cs.umd.edu/~gasarch/pcp/AS.pdf
"Proof Verification and the Hardness of Approximation Problems". Sanjeev Arora, Carsten Lund, Rajeev Motwani, Madhu Sudan, and Mario Szegedy. Journal of the ACM 45 (1998), 501-555.
https://web.archive.org/web/20110610101241/https://www.cs.umd.edu/~gasarch/pcp/ALMSS.pdf

2000: Moshe Vardi and Pierre Wolper

The 2000 Gödel Prize is awarded to
Moshe Vardi and Pierre Wolper for their paper:
Reasoning about infinite computations. Moshe Y. Vardi, Pierre Wolper. Information and Computation 115 (1994), 1-37.
https://web.archive.org/web/20110825210914/http://reference.kfupm.edu.sa/content/r/e/reasoning_about_infinite_computations__102167.pdf

1999: Peter W. Shor

The 1999 Gödel Prize for outstanding journal article in the area of theoretical computer science is awarded to
Peter W. Shor for his paper "Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer", SIAM Journal on Computing 26 (1997), 1484-1509.
https://arxiv.org/pdf/quant-ph/9508027.pdf

1998: Seinosuke Toda

The 1998 Gödel Prize for outstanding journal article in the area of theoretical computer science will be awarded to
Seinosuke Toda for his paper "PP is as Hard as the Polynomial-Time Hierarchy," SIAM Journal on Computing 20 (1991), 865-877.
https://people.engr.tamu.edu/j-chen3/courses/637/2008/pres/korben.pdf

1997: Joseph Halpern and Yoram Moses

The 1997 Gödel Prize for outstanding journal articles in the area of theoretical computer science will be awarded to
Joseph Halpern and Yoram Moses for their paper "Knowledge and Common Knowledge in a Distributed Environment," J. ACM 37} (1990), 549-587.
https://www.cs.cornell.edu/home/halpern/papers/common_knowledge.pdf

1996: Mark Jerrum and Alistair Sinclair

The 1996 Gödel Prize for outstanding journal articles in the area of theoretical computer science was awarded on May 23, 1996 jointly to
Mark Jerrum and Alistair Sinclair for their papers "Approximate counting, unform generation and rapidly mixing Markov chains," Information and Computation 82 (1989), 93-133, by Sinclair and Jerrum,
https://reader.elsevier.com/reader/sd/pii/0890540189900679?token=518EF4273B015187831CB0A883A601D699224964F2F448061BEE0B856FC0FE6A24FCDD1567B81553115DC281EB962793
and
"Approximating the permanent," SIAM Journal on Computing 18 (1989), 1149-1178, by Jerrum and Sinclair.
https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.431.4190&rep=rep1&type=pdf

1995: Neil Immerman and Róbert Szelepcsényi

The Gödel prize committee has selected the co-recipients of the Gödel Prize for 1995. The prize is awarded for the following two papers:
Neil Immerman, "Nondeterministic space is closed under complementation," SIAM Journal on Computing 17 (1988), 935-938
https://people.cs.umass.edu/~immerman/pub/space.pdf
and
Róbert Szelepcsényi, "The method of forced enumeration for nondeterministic automata," Acta Informatica 26 (1988), 279-284.
https://dml.cz/bitstream/handle/10338.dmlcz/120489/ActaOstrav_03-1995-1_10.pdf

1994: Johan Håstad

Johan Håstad, "Almost optimal lower bounds for small depth circuits," Advances in Computing Research 5 (1989), 143-170.
https://web.archive.org/web/20120222163102/http://reference.kfupm.edu.sa/content/a/l/almost_optimal_lower_bounds_for_small_de_134215.pdf

1993: László Babai, Shafi Goldwasser, Silvio Micali, Shlomo Moran, and Charles Rackoff

The 1993 Gödel Prize was shared by two papers,
László Babai and Shlomo Moran, "Arthur-Merlin games: a randomized proof system and a hierarchy of complexity classes," Journal of Computer and System Sciences, 36 (1988), 254-276,
http://crypto.cs.mcgill.ca/~crepeau/COMP647/2007/TOPIC01/AMgames-Babai-Moran.pdf
and
Shafi Goldwasser, Silvio Micali, and Charles Rackoff, "The knowledge complexity of interactive proof systems," SIAM Journal on Computing 18 (1989), 186-208.
http://crypto.cs.mcgill.ca/~crepeau/COMP647/2007/TOPIC02/GMR89.pdf

#作業場(work space)

まずゲーテルの論文の単語帳。

自分のPCにあるフォルダ名が
/Users/administrator/Downloads/godel
の場合

shell

$ docker run -v /Users/administrator/Downloads/godel:/tmp/godel -it kaizenjapan/godel /bin/bash

いつもは上位１００語を表示する。
数式が多く、１語は式でしか現れないかもしれない。
１０語以上だと上位１３６位まで。
整列は表計算ソフトに読み込んで並べ替えをした。

work	count
the	413
x	395
of	255
a	237
is	211
n	182
y	159
and	146
to	120
that	119
for	112
v	106
in	102
r	80
we	77
by	75
i	73
z	71
not	69
are	66
number	63
this	59
p	58
formula	55
it	51
provable	49
q	48
primitive	47
one	46
as	44
be	43
if	43
with	43
forall	41
sign	39
axiom	37
length	37
class	36
k	36
free	35
item	35
or	35
recursive	35
from	34
subst	34
which	34
there	33
an	32
proof	32
relation	31
type	31
system	30
theorem	30
formulae	29
variable	29
all	28
numbers	28
where	28
will	28
can	27
e	27
you	27
axioms	26
on	26
s	25
xn	25
b	24
have	23
every	22
natural	22
paper	22
succ	22
other	21
such	21
but	19
following	19
sequence	19
go	18
translation	18
would	18
also	17
rq	17
u	17
consistency	16
consistent	16
del	16
then	16
basic	15
finite	15
text	15
undecidable	15
variables	15
any	14
defined	14
function	14
has	14
pm	14
seq	14
signs	14
argmin	13
because	13
call	13
concepts	13
does	13
now	13
only	13
first	12
formal	12
holds	12
more	12
no	12
prooffor	12
used	12
was	12
at	11
decision	11
define	11
fact	11
functions	11
its	11
let	11
schema	11
set	11
so	11
systems	11
these	11
c	10
example	10
hand	10
my	10
obtained	10
proposition	10
quantor	10
relations	10
some	10
well	10

受賞論文

２論文が未入手、２論文が事前投稿論文。
式の中に２文字の記号を含むと仮定すると
676語は式中の記号の可能性がある。

ひとまず出現頻度が100までの683語を示す。

残りは、最後に記載したのDocker Hub上にファイルあり。

ubuntu/bash

./ptt.sh
cat text/* > all.txt
 awk -f wc.awk all.txt > wc.txt

word	count	note
the	29214
a	19144
of	18139
and	11769
is	11715
in	10220
y	9933
f	9700
i	9139
to	9012
x	8913
that	8803
b	8657
s	8465
n	8129
h	7348
we	7335
u	7322
for	6999
q	6720
p	5916
c	5906
g	5442
k	5207
m	4554
e	4407
v	4307
by	4258
t	4257
d	4090
be	4043
j	4022
this	3882
r	3542
l	3330
as	3196
with	3119
on	3094
an	2935
if	2741
it	2565
are	2553
let	2399
then	2198
at	2137
w	2051
proof	2000
from	1929
can	1921
z	1873
lemma	1717
which	1700
o	1692
not	1646
all	1577
such	1562
have	1509
each	1419
log	1411
set	1407
theorem	1394
where	1315
there	1278
algorithm	1201
some	1187
one	1186
random	1172
time	1143
any	1132
will	1130
our	1090
probability	1053
or	1041
every	1019
has	998
_	993
polynomial	959
number	957
case	920
two	895
given	887
only	883
bi	856
since	844
graph	825
so	823
function	821
most	802
problem	776
these	743
when	739
using	722
section	719
also	715
its	714
follows	710
de	696
first	683
now	682
use	677
following	661
size	649
least	645
us	639
computer	635
input	624
ii	616
than	615
thus	611
value	611
system	599
more	594
over	594
but	592
no	589
show	588
see	587
linear	575
hence	548
prove	543
state	543
other	529
definition	518
same	512
pp	511
note	509
xu	507
science	505
np	504
above	503
may	503
free	495
ca	477
do	475
variables	459
vertex	459
constant	457
result	448
bound	446
consider	442
new	441
problems	435
algorithms	433
TRUE	429
approximation	428
verifier	425
paper	424
does	421
protocol	421
assume	413
deterministic	411
was	409
step	407
vol	407
exists	398
between	397
degree	397
th	395
complexity	394
denote	391
point	390
xi	390
output	389
define	384
pr	384
si	383
edges	381
example	380
edge	379
resource	379
used	376
fact	373
theory	371
values	371
must	366
graphs	361
bits	357
oracle	357
both	351
max	351
length	349
assignment	345
functions	343
their	342
form	339
key	339
would	336
they	335
process	334
results	331
computing	328
matrix	327
work	327
defined	325
acm	324
condition	323
under	318
list	316
proofs	316
test	316
possible	315
way	314
min	313
lower	311
systems	311
suppose	307
mod	306
property	306
here	304
cost	303
small	303
order	301
instance	300
into	300
get	298
sequence	297
tree	296
how	294
distribution	292
second	291
well	291
whose	289
un	288
emp	287
wi	287
non	286
however	285
obtain	283
ai	281
implies	281
ui	280
within	280
been	279
vi	279
need	278
vertices	277
map	275
factor	273
quantum	273
based	272
access	271
complex	271
part	270
optimal	269
model	267
points	266
even	265
independent	265
analysis	264
make	261
nite	261
symposium	261
about	260
simplex	260
vector	260
al	259
because	259
bounded	256
path	253
proceedings	253
computation	252
sum	252
yjv	252
say	251
sets	251
string	251
variable	251
class	250
program	248
corresponding	246
large	246
main	245
while	245
hard	244
ud	244
udc	244
depth	243
automata	241
known	241
procedure	241
automaton	240
construction	239
natural	236
sj	236
accepts	235
bit	235
bounds	235
either	234
formula	234
ta	234
give	233
theoretical	233
particular	232
logic	231
object	231
objects	228
general	227
check	226
nition	225
last	223
many	221
chosen	220
space	220
proposition	218
udy	218
otherwise	217
simple	217
zero	216
et	215
notion	213
states	213
ratio	212
sorted	212
properties	211
local	210
product	210
interactive	209
parallel	209
call	208
approximate	207
equations	207
complete	206
full	206
claim	204
di	204
holds	203
integer	203
ti	203
find	202
finite	202
next	202
ne	201
satisfying	200
inequality	199
pi	199
similar	199
up	199
xud	199
ia	198
close	197
just	197
mechanism	197
poly	196
annual	195
hhv	195
processes	195
recall	195
circuit	193
gives	193
unsat	193
left	192
weight	192
choose	191
conditions	191
task	191
therefore	190
very	190
flow	188
ned	188
corollary	187
times	187
arbitrary	186
called	185
line	185
standard	185
subdivision	185
top	185
proc	183
compute	182
cannot	181
queries	181
uniform	181
contains	180
expected	180
structure	180
ieee	179	Institute of Electrical and Electronics Engineers
probabilistic	179
running	179
chain	178
languages	178
enizergues	177	human name
induction	177
language	177
group	176
shown	176
reduction	175
type	175
code	174
distance	174
information	174
obtained	174
required	174
rule	173
agent	172
describe	172
without	171
after	170
construct	170
figure	170
exactly	169
should	169
assumption	168
cau	168
could	168
hypothesis	168
satis	168
what	168
almost	167
positive	167
matrices	166
three	166
uses	166
grade	165
satisfies	165
described	164
below	162
fixed	162
good	162
nu	162
out	162
ri	162
solution	162
version	162
knowledge	160
pair	160
terms	160
counting	159
different	159
whether	159
alphabet	158
connected	158
constraint	158
ji	158
siam	158	Society for Industrial and Applied Mathematics
vectors	158
choice	157
clearly	157
efficient	157
sat	157
steps	157
agents	156
cs	156	computer science
inputs	156
pages	156
programs	156
those	156
public	154
shows	153
special	152
them	152
easy	151
fraction	151
less	151
proved	151
approximating	150
pcp	150
apply	149
decision	149
high	149
notation	149
right	149
scheme	149
similarly	149
am	147
before	147
prover	147
abort	146
cases	146
were	146
another	145
cut	145
finally	145
know	145
through	145
discrete	144
id	144	identifier
method	144
arora	143
au	142
outputs	142
constraints	141
ei	141
error	141
view	141
elements	140
makes	140
rst	140
regular	139
rules	139
subset	139
takes	139
fp	138
lattice	138
memory	138
optimality	138
prime	138
much	137
relation	137
requires	136
single	136
again	135
being	135
equivalent	135
series	135
hand	134
satisfy	134
nodes	133
partition	133
programming	133
boolean	132
gf	132
observe	132
st	132
total	132
vb	132
words	132
field	131
game	131
machine	131
self	131
write	131
answer	130
numbers	130
power	130
real	130
argument	129
basic	129
database	129
done	129
might	129
owned	129
run	129
take	129
able	128
accept	128
curve	128
seen	128
springer	128
start	128
useful	128
circuits	127
equal	127
moreover	127
present	127
always	126
pairing	126
entries	125
markov	125
put	125
accesses	124
comput	124
level	124
merlin	124
original	124
remark	124
context	123
combinatorial	122
dom	122
further	122
idea	122
nd	122
tsp	122
ci	121
cr	121
execution	121
notes	121
simplicial	121
xk	121
aw	120
exist	120
low	120
randomized	120
rather	120
aggregation	119
applications	119
formal	119
notice	119
operations	119
exp	118
family	118
inv	118
perfect	118
query	118
sense	118
upper	118
aq	117
bk	117
restriction	117
square	117
trace	117
transition	117
approach	116
equation	116
polynomials	116
root	116
heap	115
word	115
conclude	113
encoding	113
hardness	113
made	113
maximum	113
previous	113
techniques	113
uj	113
element	112
private	112
separation	112
simply	112
strategy	112
design	111
event	111
journal	111
lists	111
nc	111
writes	111
arthur	110
encryption	110
er	110
instances	110
ny	110
soundness	110
yj	110
chromatic	109
equivalence	109
generator	109
li	109
models	109
nonzero	109
respectively	109
completeness	108
dl	108
lecture	108
security	108
acceptance	107
buf	107
bw	107
open	107
checking	106
classes	106
iff	106
minimum	106
tb	106
formulas	105
important	105
initial	105
read	105
side	105
unique	105
xn	105
conductance	104
latency	104
paths	104
appear	103
bn	103
boundary	103
distinct	103
oracles	103
sequential	103
still	103
strings	103
accepting	102
ap	102
computed	102
long	102
node	102
question	102
associated	101
easily	101
im	101
udn	101
gate	100
like	100
matching	100
means	100
ownership	100
partial	100
provided	100
row	100
symmetric	100
weighted	100

tools

単語出現頻度計数

wc.awk

# Print list of word frequencies
# https://researchmap.jp/jomd7nobo-45644/
# https://qiita.com/kaizen_nagoya/items/670d4d332e07fd2e5fc2
# This is for papers, not for programming.
# remove _ from gsub list 20200101 @kaizen_nagoya

{
    $0 = tolower($0)    # 
    gsub(/[^a-z \t]/, " ", $0)  #
    for (i = 1; i <= NF; i++)
        freq[$i]++
}

END {
    for (word in freq)
        printf "%s\t%d\n", word, freq[word]
}

一括処理

ptt.sh

#!/bin/bash
# https://news.mynavi.jp/article/bashonwindows-17/
# https://qiita.com/kaizen_nagoya/items/319672853519990cee42

 cd ../pdf
 for File in *; do
    case ${File##*.} in
        pdf|PDF )
            echo "Convert the PDF:" ${File}
            pdftotext -q ${File} ../text/${File}.txt ;;
        *) ;;
    esac
 done

docker hub登録

docker 起動（最初）

shell

$ docker run -v /Users/administrator/Downloads/godel:/tmp/godel -it ubuntu /bin/bash

dockerでの作業

ubuntu/bash

# apt update; apt -y upgrade
# apt install -y poppler-utils vim wget
# wget http://hirzels.com/martin/papers/canon00-goedel.pdf
# pdftotext -q  canon00-goedel.pdf canon00-goedel.txt
# awk -f wc.awk canon00-goedel.txt >godelwc.txt

docker hub 登録

bash

$ docker commit 7aa98d94d8da kaizenjapan/godel 
$ docker push kaizenjapan/godel

次回起動

shell

$ docker run -v /Users/administrator/Downloads/godel:/tmp/godel -it kaizenjapan/godel /bin/bash

文書履歴(document history)

ver. 0.01 初稿 20201020
ver. 0.02 ゲーデル論文URL記載 20201024午前
ver. 0.03 ゲーテル論文単語帳 20201024午後
ver. 0.04 単語帳作成、docker登録 20201024 夜
ver. 0.05 Reference 追記 20201025