Suggested Papers

Paper	Suggested By	Added On
Liu, J. et al. (2019). Formal Verification of Quantum Algorithms Using Quantum Hoare Logic	Christine	2024-10-22
Filip Sieczkowski, Sergei Stepanenko, Jonathan Sterling, Lars Birkedal. 2024. The Essence of Generalized Algebraic Data Types. POPL'24	Zilin	2023-12-05
Zohar Manna and Richard Waldinger. 1980. A Deductive Approach to Program Synthesis. ACM Trans. Program. Lang. Syst. 2, 1 (Jan. 1980), 90–121. https://doi.org/10.1145/357084.357090	Zilin
Shayan Najd, Sam Lindley, Josef Svenningsson, and Philip Wadler. 2016. Everything old is new again: quoted domain-specific languages. In Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM '16). Association for Computing Machinery, New York, NY, USA, 25–36. DOI:https://doi.org/10.1145/2847538.2847541	Zilin
Michael Ballantyne, Alexis King, and Matthias Felleisen. 2020. Macros for Domain-Specific Languages. Proc. ACM Program. Lang. 4, OOPSLA, Article 229 (November 2020), 29 pages. https://doi.org/10.1145/3428297	Zilin
Mahshid Shahmohammadian and Geoffrey Mainland. 2021. Metaprogramming with Combinators. In Proceedings of the 20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE ’21), October 17–18, 2021, Chicago, IL, USA. ACM, New York, NY, USA, 12 pages. https://doi.org/10.1145/3486609.3487198	Zilin
Lionel Parreaux, Amir Shaikhha, Christoph E. Koch. 2017. Squid: Type-Safe, Hygienic, and Reusable Quasiquotes. In Proceedings of 8th ACM SIGPLAN International Scala Symposium (SCALA’17). ACM, New York, NY, USA, 11 pages. https://doi.org/10.1145/3136000.3136005	Zilin
Aaron Turon, Derek Dreyer, and Lars Birkedal. 2013. Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. SIGPLAN Not. 48, 9 (September 2013), 377–390. DOI:https://doi.org/10.1145/2544174.2500600	Selene
Mads Tofte, Jean-Pierre Talpin. 1997. Region-Based Memory Management. Information and Computation, Volume 132, Issue 2, 1997. pp 109‒176, ISSN 0890-5401, DOI=https://doi.org/10.1006/inco.1996.2613.
Csaba Hruska , Péter Dávid Podlovics , and Andor Pénzes. 2019. A modern look at GRIN, an optimizing functional language back end.
Donald W. Loveland. 1968. Mechanical Theorem-Proving by Model Elimination. J. ACM 15, 2 (April 1968), 236–251. DOI:https://doi.org/10.1145/321450.321456
Noam Zeilberger. 2008. Focusing and Higher-Order Abstract Syntax. In POPL'08.
Peter Lammich. 2019. Generating Verified LLVM from Isabelle/HOL. 10th International Conference on Interactive Theorem Proving (ITP 2019). DOI=https://doi.org/10.4230/LIPIcs.ITP.2019.22
Oukseh Lee and Kwangkeun Yi. 1998. Proofs about a folklore let-polymorphic type inference algorithm. ACM Trans. Program. Lang. Syst. 20, 4 (July 1998), 707–723. DOI:https://doi.org/10.1145/291891.291892
Farmer W.M. (2016) Incorporating Quotation and Evaluation into Church’s Type Theory: Syntax and Semantics. CICM 2016. Lecture Notes in Computer Science, vol 9791. DOI:https://doi.org/10.1007/978-3-319-42547-4_7	Vincent
Kaposi A., Kovács A., Kraus N. 2019. Shallow Embedding of Type Theory is Morally Correct. MPC 2019. Lecture Notes in Computer Science, vol 11825. DOI:https://doi.org/10.1007/978-3-030-33636-3_12
Harvey Tuch, Gerwin Klein, and Michael Norrish. 2007. Types, bytes, and separation logic. SIGPLAN Not. 42, 1 (January 2007), 97–108. DOI:https://doi.org/10.1145/1190215.1190234
J. Nagele, V. van Oostrom, C. Sternagel. (2016). A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property for the λβ-calculus in Nominal Isabelle. https://arxiv.org/abs/1609.03139
McBride C. (2015) Turing-Completeness Totally Free. In: Hinze R., Voigtländer J. (eds) Mathematics of Program Construction. MPC 2015. Lecture Notes in Computer Science, vol 9129. Springer, Cham. DOI=https://doi.org/10.1007/978-3-319-19797-5\_13
Emina Torlak and Rastislav Bodik. 2014. A lightweight symbolic virtual machine for solver-aided host languages. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '14). ACM, New York, NY, USA, 530-541. DOI:https://doi.org/10.1145/2594291.2594340
P. J. Landin. 1966. The next 700 programming languages. Commun. ACM 9, 3 (March 1966), 157-166. DOI=http://dx.doi.org/10.1145/365230.365257
Huet, G. P. (1975). A Unification Algorithm for Typed λ-calculus. Theoretical Computer Science 1. pp. 27–57.
Tiuryn, J. (1990). Type Inference Problems: A Survey. Mathematical Foundations of Computer Science. pp 105–120
Gentzen, G. (1964). Investigations into Logical Deduction. American Philosophical Quarterly, Vol.1(4). pp. 288–306
Wigner, E. P. (1960), The unreasonable effectiveness of mathematics in the natural sciences. Richard courant lecture in mathematical sciences delivered at New York University, May 11, 1959. Comm. Pure Appl. Math., 13: 1–14. doi:https://doi.org/10.1002/cpa.3160130102
Halpern, J., et al. (2001). On the Unusual Effectiveness of Logic in Computer Science. Bulletin of Symbolic Logic, 7(2), 213–236. doi:10.2307/2687775
Peyton Jones, S. (2006). Haskell Is Not Not ML. European Symposium on Programming, ESOP. pp. 38–53
Timothy G. Griffin. (1989). A formulae-as-type notion of control. POPL '90.
Chen, C and Hudak, P. (1997). Rolling Your Own Mutable ADT — A Connection Between Linear Types and Monads. Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages,  POPL '97. pp. 54--66. doi:10.1145/263699.263708
An excerpt from Kleene's Introduction to Metamathematics. For example. Chapter III, A critique of mathematical reasoning. pp 36–65, which covers paradoxes, logicism, intuitionism, formalism, etc.
Something on paraconsistency
Luis Damas and Robin Milner. 1982. Principal type-schemes for functional programs. In Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL '82). ACM, New York, NY, USA, 207-212. DOI=http://dx.doi.org/10.1145/582153.582176
John McCarthy. 1960. Recursive functions of symbolic expressions and their computation by machine, Part I. Commun. ACM 3, 4 (April 1960), 184-195. DOI: https://doi.org/10.1145/355602.361309
Gerard P. Huet. 1973. The undecidability of unification in third order logic. Information and Control, Volume 22, Issue 3, pp 257–267. ISSN 0019-9958. https://doi.org/10.1016/S0019-9958(73)90301-X.
D. L. Parnas. 1972. A technique for software module specification with examples. Commun. ACM 15, 5 (May 1972), 330-336. DOI:https://doi.org/10.1145/355602.361309
F.L. Morris and C.B. Jones. 1984. An Early Program Proof by Alan Turing. Annals of the History of Computing, Volume: 6 , Issue: 2 , April-June 1984. pp. 139–143. DOI: https://doi.org/10.1109/MAHC.1984.10017
Lars Hupel, Tobias Nipkow. 2018. A Verified Compiler from Isabelle/HOL to CakeML. ESOP'18. https://link.springer.com/chapter/10.1007%2F978-3-319-89884-1_35
Karl Crary. Fully Abstract Module Compilation. 2019 Symposium on Principles of Programming Languages.
Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. 2016. Push-button verification of file systems via crash refinement. In Proceedings of the 12th USENIX conference on Operating Systems Design and Implementation (OSDI'16). USENIX Association, Berkeley, CA, USA, 1-16.
Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. 2017. Hyperkernel: Push-Button Verification of an OS Kernel. In Proceedings of the 26th Symposium on Operating Systems Principles (SOSP '17). ACM, New York, NY, USA, 252-269. DOI: https://doi.org/10.1145/3132747.3132748