sample.bib

@InCollection{BaaderSnyder01,
  title =	"Unification Theory",
  author =	"Franz Baader and Wayne Snyder",
  bibdate =	"2021-04-09",
  bibsource =	"DBLP,
		 http://dblp.uni-trier.de/db/books/collections/RobinsonV01.html#BaaderS01;
		 DBLP,
		 http://dblp.uni-trier.de/https://doi.org/10.1016/b978-044450813-3/50010-2",
  booktitle =	"Handbook of Automated Reasoning",
  booktitle =	"Handbook of Automated Reasoning (in 2 volumes)",
  publisher =	"Elsevier and MIT Press",
  year = 	"2001",
  editor =	"John Alan Robinson and Andrei Voronkov",
  ISBN = 	"0-444-50813-9; 0-262-18223-8",
  pages =	"445--462",
  url = "https://www.cs.bu.edu/fac/snyder/publications/UnifChapter.pdf",
}

@InCollection{Tarski1956,
  author =	"Alfred Tarski",
  title =	"The Concept of Truth in Formalized Languages",
  booktitle =	"Logic, Semantics, Metamathematics",
  publisher =	"Oxford University Press",
  year = 	"1956",
  editor =	"Alfred Tarski",
  pages =	"152--278",
  address =	"Oxford",
  note = 	"Translated by J.H. Woodger",
  xref = 	"English translation of: tarski_a:1936a2.",
  topic =	"foundations-of-semantics;truth;logic-classic;semantic-paradoxes;",
}

@article{Krivine07,
    title = {A call-by-name lambda-calculus machine},
    volume = {20},
    url = {http://link.springer.com/10.1007/s10990-007-9018-9},
    doi = {10.1007/s10990-007-9018-9},
    number = {3},
    journal = {Higher-Order and Symbolic Computation},
    author = {Krivine, Jean-Louis},
    year = {2007},
    pages = {199--207}
}

@article{Landin64SECD,
    author = {Landin, P. J.},
    title = "{The Mechanical Evaluation of Expressions}",
    journal = {The Computer Journal},
    volume = {6},
    number = {4},
    pages = {308-320},
    year = {1964},
    month = {01},
    abstract = "{This paper is a contribution to the “theory” of the activity of using computers. It shows how some forms of expression used in current programming languages can be modelled in Church's λ-notation, and then describes a way of “interpreting” such expressions. This suggests a method, of analyzing the things computer users write, that applies to many different problem orientations and to different phases of the activity of using a computer. Also a technique is introduced by which the various composite information structures involved can be formally characterized in their essentials, without commitment to specific written or other representations.}",
    issn = {0010-4620},
    doi = {10.1093/comjnl/6.4.308},
    url = {https://doi.org/10.1093/comjnl/6.4.308},
    eprint = {https://academic.oup.com/comjnl/article-pdf/6/4/308/1067901/6-4-308.pdf},
}

@inproceedings{Felleisen87CESK,
author = {Felleisen, Mattias and Friedman, D. P.},
title = {A Calculus for Assignments in Higher-Order Languages},
year = {1987},
isbn = {0897912152},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/41625.41654},
doi = {10.1145/41625.41654},
abstract = {Imperative assignments are abstractions of recurring programming patterns in purely functional programming languages. When added to higher-order functional languages, they provide a higher-level of modularity and security but invalidate the simple substitution semantics. We show that, given an operational interpretation of a denotational semantics for such a language, it is possible to design a two-level extension of the λu-calculus. This calculus provides a location-free rewriting semantics of the language and offers new possibilities for reasoning with assignments. The upper level of the calculus factors out all the steps in a reduction sequence which must be in a linear order; the lower level allows a partial ordering of reduction steps.},
booktitle = {Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages},
pages = {314},
location = {Munich, West Germany},
series = {POPL '87}
}

@InProceedings{Felleisen86a,
  author =	"Matthias Felleisen and Daniel P. Friedman",
  title =	"Control operators, the {SECD}-machine, and the $\lambda$-calculus",
  booktitle =	"3rd Working Conference on the Formal Description of Programming Concepts",
  pages =	"193--219",
  address =	"Ebberup, Denmark",
  month =	8,
  year = 	"1986",
}

@inproceedings{Reynolds1974PolyLambda,
author = {Reynolds, John C.},
title = {Towards a Theory of Type Structure},
year = {1974},
isbn = {3540068597},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
booktitle = {Programming Symposium, Proceedings Colloque Sur La Programmation},
pages = {408–423},
numpages = {16}
}


@InCollection{Girard1971,
  author =	"Jean-Yves Girard",
  title =	"Une Extension de l'Interpr{\'e}tation de {G}{\"o}del
		 {\`a} l'Analyse, et son Application {\`a}
		 l'{{\'E}}limination des Coupures dans l'Analyse et la
		 Th{\'e}orie des Types",
  editor =	"J. E. Fenstad",
  booktitle =	"Proceedings 2nd Scandinavian Logic Symp., Oslo,
		 Norway, 18--20 June 1970",
  series =	"Studies in Logic and the Foundations of Mathematics",
  volume =	"63",
  pages =	"63--92",
  publisher =	"North-Holland",
  address =	"Amsterdam",
  year = 	"1971",
}

@PhdThesis{Girard1972,
  author =	"Jean-Yves Girard",
  title =	"Interpr\'{e}tation fonctionelle et \'{e}limination des
		 coupures dans l'arithm\'{e}tique d'ordre
		 sup\'{e}rieur",
  school =	"University of Paris VII",
  year = 	"1972",
}

@article{BoehmBerarducci1985,
	abstract = {The notion of iteratively defined functions from and to heterogeneous term algebras is introduced as the solution of a finite set of equations of a special shape. Such a notion has remarkable consequences: (1) Choosing the second-order typed lamdda-calculus (\ensuremath{\Lambda} for short) as a programming language enables one to represent algebra elements and iterative functions by automatic uniform synthesis paradigms, using neither conditional nor recursive constructs. (2) A completeness theorem for \ensuremath{\Lambda}-terms with type of degree at most two and a companion corollary for \ensuremath{\Lambda}-programs have been proved. (3) A new congruence relation for the last-mentioned \ensuremath{\Lambda}-terms which is stronger than \ensuremath{\Lambda}-convertibility is introduced and proved to have the meaning of a \ensuremath{\Lambda}-program equivalence. Moreover, an extension of the paradigms to the synthesis of functions of higher complexity is considered and exemplified. All the concepts are explained and motivated by examples over integers, list- and tree-structures.},
	author = {Corrado Böhm and Alessandro Berarducci},
	doi = {10.1016/0304-3975(85)90135-5},
	issn = {0304-3975},
	journal = {Theoretical Computer Science},
	note = {Third Conference on Foundations of Software Technology and Theoretical Computer Science},
	pages = {135–154},
	title = {Automatic synthesis of typed \ensuremath{\Lambda}-programs on term algebras},
	url = {https://www.sciencedirect.com/science/article/pii/0304397585901355},
	volume = {39},
	year = {1985}
}

@ARTICLE{Wright2010cacm,
  title    = "Linear logic",
  author   = "Wright, Alex",
  journal  = "Commun. ACM",
  volume   =  53,
  number   =  10,
  pages    = "11--13",
  year     =  2010,
  language = "en"
}

@TechReport{Plotkin1981sos,
  author =	"Gordon D. Plotkin",
  title =	"A Structural Approach to Operational Semantics",
  address =	"Aarhus, Denmark",
  institution =  "Computer Science Department, Aarhus University",
  year = 	"1981",
  month =	9,
  number =	"DAIMI FN--19",
}

@article{Hutton2021easy123,
  title={Programming Language Semantics: it's easy as 1,2,3},
  author={Hutton, Graham},
  year =2001,
  note ={draft},
}

@BOOK{Hutton2016pih2nd,
  title     = "Programming in Haskell",
  author    = "Hutton, Graham",
  publisher = "Cambridge University Press",
  year      =  2016,
  address   = "Cambridge, England"
}

@article{deBruijn1972,
	abstract = {In ordinary lambda calculus the occurrences of a bound variable are made recognizable by the use of one and the same (otherwise irrelevant) name at all occurrences. This convention is known to cause considerable trouble in cases of substitution. In the present paper a different notational system is developed, where occurrences of variables are indicated by integers giving the “distance” to the binding \ensuremath{\lambda} instead of a name attached to that \ensuremath{\lambda}. The system is claimed to be efficient for automatic formula manipulation as well as for metalingual discussion. As an example the most essential part of a proof of the Church-Rosser theorem is presented in this namefree calculus.},
	author = {N.G {de Bruijn}},
	doi = {10.1016/1385-7258(72)90034-0},
	issn = {1385-7258},
	journal = {Indagationes Mathematicae (Proceedings)},
	number = {5},
	pages = {381–392},
	title = {Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem},
	url = {https://www.sciencedirect.com/science/article/pii/1385725872900340},
	volume = {75},
	year = {1972}
}

@article{Ramsdell1989alonzo,
author = {Ramsdell, J. D.},
title = {The Alonzo Functional Programming Language},
year = {1989},
issue_date = {Sept. 1989},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {24},
number = {9},
issn = {0362-1340},
url = {https://doi.org/10.1145/68127.68139},
doi = {10.1145/68127.68139},
abstract = {Alonzo is a programming language for specifying an output stream of characters as a function of a given input stream of characters. It is a non-strict language based on the untyped λ-calculus, and it has been enriched by adding syntax for local bindings and mutual recursion. Primitive data and their operators have been included along with strict vectors.},
journal = {SIGPLAN Not.},
month = {10},
pages = {152–157},
numpages = {6}
}


@InProceedings{Seijas2020Marlowe,
author="Lamela Seijas, Pablo
and Nemish, Alexander
and Smith, David
and Thompson, Simon",
editor="Bernhard, Matthew
and Bracciali, Andrea
and Camp, L. Jean
and Matsuo, Shin'ichiro
and Maurushat, Alana
and R{\o}nne, Peter B.
and Sala, Massimiliano",
title="Marlowe: Implementing and Analysing Financial Contracts on Blockchain",
booktitle="Financial Cryptography and Data Security",
year="2020",
publisher="Springer International Publishing",
address="Cham",
pages="496--511",
abstract="Marlowe is a DSL for financial contracts. We describe the implementation of Marlowe on the Cardano blockchain, and the Marlowe Playground web-based development and simulation environment.",
isbn="978-3-030-54455-3"
}

@inproceedings{Hudak2007HistoryHaskell,
author = {Hudak, Paul and Hughes, John and Peyton Jones, Simon and Wadler, Philip},
title = {A History of Haskell: Being Lazy with Class},
year = {2007},
isbn = {9781595937667},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/1238844.1238856},
doi = {10.1145/1238844.1238856},
abstract = {This paper describes the history of Haskell, including its genesis and principles, technical contributions, implementations and tools, and applications and impact.},
booktitle = {Proceedings of the Third ACM SIGPLAN Conference on History of Programming Languages},
pages = {12–1–12–55},
location = {San Diego, California},
series = {HOPL III}
}

@inproceedings{FreshML2003,
author = {Shinwell, Mark R. and Pitts, Andrew M. and Gabbay, Murdoch J.},
title = {FreshML: Programming with Binders Made Simple},
year = {2003},
isbn = {1581137567},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/944705.944729},
doi = {10.1145/944705.944729},
abstract = {FreshML extends ML with elegant and practical constructs for declaring and manipulating syntactical data involving statically scoped binding operations. User-declared FreshML datatypes involving binders are concrete, in the sense that values of these types can be deconstructed by matching against patterns naming bound variables explicitly. This may have the computational effect of swapping bound names with freshly generated ones; previous work on FreshML used a complicated static type system inferring information about the 'freshness' of names for expressions in order to tame this effect. The main contribution of this paper is to show (perhaps surprisingly) that a standard type system without freshness inference, coupled with a conventional treatment of fresh name generation, suffices for FreshML's crucial correctness property that values of datatypes involving binders are operationally equivalent if and only if they represent a-equivalent pieces of object-level syntax. This is established via a novel denotational semantics. FreshML without static freshness inference is no more impure than ML and experience with it shows that it supports a programming style pleasingly close to informal practice when it comes to dealing with object-level syntax modulo a-equivalence.},
booktitle = {Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming},
pages = {263–274},
numpages = {12},
keywords = {metaprogramming, variable binding, alpha-conversion},
location = {Uppsala, Sweden},
series = {ICFP '03}
}

@article{Unbound2011,
author = {Weirich, Stephanie and Yorgey, Brent A. and Sheard, Tim},
title = {Binders Unbound},
year = {2011},
issue_date = {September 2011},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {46},
number = {9},
issn = {0362-1340},
url = {https://doi.org/10.1145/2034574.2034818},
doi = {10.1145/2034574.2034818},
abstract = {Implementors of compilers, program refactorers, theorem provers, proof checkers, and other systems that manipulate syntax know that dealing with name binding is difficult to do well. Operations such as α-equivalence and capture-avoiding substitution seem simple, yet subtle bugs often go undetected. Furthermore, their implementations are tedious, requiring "boilerplate" code that must be updated whenever the object language definition changes.Many researchers have therefore sought to specify binding syntax declaratively, so that tools can correctly handle the details behind the scenes. This idea has been the inspiration for many new systems (such as Beluga, Delphin, FreshML, FreshOCaml, Cαml, FreshLib, and Ott) but there is still room for improvement in expressivity, simplicity and convenience.In this paper, we present a new domain-specific language, Unbound, for specifying binding structure. Our language is particularly expressive - it supports multiple atom types, pattern binders, type annotations, recursive binders, and nested binding (necessary for telescopes, a feature found in dependently-typed languages). However, our specification language is also simple, consisting of just five basic combinators. We provide a formal semantics for this language derived from a locally nameless representation and prove that it satisfies a number of desirable properties.We also present an implementation of our binding specification language as a GHC Haskell library implementing an embedded domain specific language (EDSL). By using Haskell type constructors to represent binding combinators, we implement the EDSL succinctly using datatype-generic programming. Our implementation supports a number of features necessary for practical programming, including flexibility in the treatment of user-defined types, best-effort name preservation (for error messages), and integration with Haskell's monad transformer library.},
journal = {SIGPLAN Not.},
month = {9},
pages = {333–345},
numpages = {13},
keywords = {patterns, generic programming, haskell, name binding}
}



@inproceedings{Sewell2007ott,
author = {Sewell, Peter and Nardelli, Francesco Zappa and Owens, Scott and Peskine, Gilles and Ridge, Thomas and Sarkar, Susmit and Strni\v{s}a, Rok},
title = {Ott: Effective Tool Support for the Working Semanticist},
year = {2007},
isbn = {9781595938152},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/1291151.1291155},
doi = {10.1145/1291151.1291155},
abstract = {It is rare to give a semantic definition of a full-scale programming language, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics - usually either LaTEX for informal mathematics, or the formal mathematics of a proof assistant - make it much harder than necessary to work with large definitions.We present a metalanguage specifically designed for this problem, and a tool, ott, that sanity-checks such definitions and compiles them into proof assistant code for Coq, HOL, Isabelle, and (in progress) Twelf, together with LaTEX code for production-quality typesetting, and OCaml boilerplate. The main innovations are:(1) metalanguage design to make definitions concise, and easy to read and edit;(2) an expressive but intuitive metalanguage for specifying binding structures; and (3) compilation to proof assistant code.This has been tested in substantial case studies, including modular specifications of calculi from the TAPL text, a Lightweight Java with Java JSR 277/294 module system proposals, and a large fragment of OCaml (around 306 rules), with machine proofs of various soundness results. Our aim with this work is to enable a phase change: making it feasible to work routinely, without heroic effort, with rigorous semantic definitions of realistic languages.},
booktitle = {Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming},
pages = {1–12},
numpages = {12},
location = {Freiburg, Germany},
series = {ICFP '07}
}

@article{Church1932,
 ISSN = {0003486X},
 URL = {http://www.jstor.org/stable/1968337},
 author = {Alonzo Church},
 journal = {Annals of Mathematics},
 number = {2},
 pages = {346--366},
 publisher = {Annals of Mathematics},
 title = {A Set of Postulates for the Foundation of Logic},
 volume = {33},
 year = {1932}
}

@article{Church1940stlc,
  title={A formulation of the simple theory of types},
  author={Church, Alonzo},
  journal={The journal of symbolic logic},
  volume={5},
  number={2},
  pages={56--68},
  year={1940},
  publisher={Cambridge University Press}
}


@inproceedings{Jeremy2006gradual,
  title={Gradual typing for functional languages},
  author={Jeremy, G Siek and Walid, Taha},
  booktitle={Scheme and Functional Programming Workshop},
  volume={6},
  pages={81--92},
  year={2006}
}

@inproceedings{Okhotin2005existence,
  title={On the existence of a Boolean grammar for a simple programming language},
  author={Okhotin, Alexander},
  booktitle={Proceedings of AFL},
  pages={17--20},
  year={2005},
  organization={Citeseer}
}

@article{Cartwright2004soft,
author = {Cartwright, Robert and Fagan, Mike},
title = {Soft Typing},
year = {2004},
issue_date = {April 2004},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {39},
number = {4},
issn = {0362-1340},
url = {https://doi.org/10.1145/989393.989435},
doi = {10.1145/989393.989435},
abstract = {Type systems are designed to prevent the improper use of program operations. They can be classified as either static or dynamic depending on when they detect type errors. Static type systems detect potential type errors at compile-time and prevent program execution. Dynamic type systems detect type errors at run-time and abort program execution.Static type systems have two important advantages over dynamic type systems. First, they help programmers detect a large class of program errors before execution. Second, they extract information that a compiler can exploit to produce more efficient code. The price paid for these advantages, however, is a loss of expressiveness, generality, and semantic simplicity.This paper presents a generalization of static and dynamic typing---called soft typing---that combines the best features of both approaches. The key idea underlying soft typing is that a static type checker need not reject programs that contain potential type errors. Instead, the type checker can insert explicit run-time checks around "suspect" arguments of primitive operations, converting dynamically typed programs into statically type-correct form. The inserted run-time checks identify program phrases that may be erroneous. For soft typing to be effective, the type system must avoid inserting unnecessary run-time checks. To accomplish this objective, we have developed an extension of the ML type system supporting union types and recursive types that assigns types to a wider class of programs than ML. We have also developed an algorithm for frugally inserting run-time checks in programs that do not type check.},
journal = {SIGPLAN Not.},
month = {4},
pages = {412–428},
numpages = {17}
}


@BOOK{Aho2013compilers2nd,
  title     = "Compilers: Pearson new international edition: Principles,
               techniques, and tools",
  author    = "Aho, A V and Lam, Monica S and Sethi, R and Ullman, Jeffrey D",
  publisher = "Pearson Education",
  edition   =  2,
  year      =  2013,
  address   = "London, England",
  language  = "en"
}

@article{Lovelace1843notes,
  title={Notes by AAL [August Ada Lovelace]},
  author={Lovelace, Ada Augusta},
  journal={Taylor's Scientific Memoirs,},
  pages={666--731},
  year={1843}
}

@article{Owens09REderivRE,
author = {Owens, Scott and Reppy, John and Turon, Aaron},
title = {Regular-Expression Derivatives Re-Examined},
year = {2009},
issue_date = {March 2009},
publisher = {Cambridge University Press},
address = {USA},
volume = {19},
number = {2},
issn = {0956-7968},
url = {https://doi.org/10.1017/S0956796808007090},
doi = {10.1017/S0956796808007090},
abstract = {Regular-expression derivatives are an old, but elegant, technique for compiling regular expressions to deterministic finite-state machines. It easily supports extending the regular-expression operators with boolean operations, such as intersection and complement. Unfortunately, this technique has been lost in the sands of time and few computer scientists are aware of it. In this paper, we reexamine regular-expression derivatives and report on our experiences in the context of two different functional-language implementations. The basic implementation is simple and we show how to extend it to handle large character sets (e.g., Unicode). We also show that the derivatives approach leads to smaller state machines than the traditional algorithm given by McNaughton and Yamada.},
journal = {J. Funct. Program.},
month = 3,
pages = {173–190},
numpages = {18}
}

@article{Brzozowski64,
author = {Brzozowski, Janusz A.},
title = {Derivatives of Regular Expressions},
year = {1964},
issue_date = {Oct. 1964},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {11},
number = {4},
issn = {0004-5411},
url = {https://doi.org/10.1145/321239.321249},
doi = {10.1145/321239.321249},
journal = {J. ACM},
month = {10},
pages = {481–494},
numpages = {14}
}

@inbook{lex1990,
author = {Lesk, M. E. and Schmidt, E.},
title = {Lex—a Lexical Analyzer Generator},
year = {1990},
isbn = {0030475295},
publisher = {W. B. Saunders Company},
address = {USA},
booktitle = {UNIX Vol. II: Research System (10th Ed.)},
pages = {375–387},
numpages = {13}
}

@book{PFPL2nd,
author = {Robert Harper},
title = {Practical Foundations for Programming Languages},
edition = 2,
year = 2016,
month = 4,
isbn = 9781107150300,
publisher = {Cambridge University Press},
}

@book{Saussure1916,
editor = {Charles Bally and Albert Sechehaye},
author = {Ferdinand de Saussure},
title = {Cours de linguistique générale},
year = 1916,
}

@inproceedings{OHearnReynoldsYang01,
author = {O'Hearn, Peter W. and Reynolds, John C. and Yang, Hongseok},
title = {Local Reasoning about Programs That Alter Data Structures},
year = {2001},
isbn = {3540425543},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
abstract = {We describe an extension of Hoare's logic for reasoning about programs that alter data structures. We consider a low-level storage model based on a heap with associated lookup, update, allocation and deallocation operations, and unrestricted address arithmetic. The assertion language is based on a possible worlds model of the logic of bunched implications, and includes spatial conjunction and implication connectives alongside those of classical logic. Heap operations are axiomatized using what we call the "small axioms", each of which mentions only those cells accessed by a particular command. Through these and a number of examples we show that the formalism supports local reasoning: A specification and proof can concentrate on only those cells in memory that a program accesses.This paper builds on earlier work by Burstall, Reynolds, Ishtiaq and O'Hearn on reasoning about data structures.},
booktitle = {Proceedings of the 15th International Workshop on Computer Science Logic},
pages = {1–19},
numpages = {19},
series = {CSL '01}
}

@inproceedings{IshtiaqOHearn01,
author = {Ishtiaq, Samin S. and O'Hearn, Peter W.},
title = {BI as an Assertion Language for Mutable Data Structures},
year = {2001},
isbn = {1581133367},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/360204.375719},
doi = {10.1145/360204.375719},
abstract = {Reynolds has developed a logic for reasoning about mutable data structures in which the pre- and postconditions are written in an intuitionistic logic enriched with a spatial form of conjunction. We investigate the approach from the point of view of the logic BI of bunched implications of O'Hearnand Pym. We begin by giving a model in which the law of the excluded middleholds, thus showing that the approach is compatible with classical logic. The relationship between the intuitionistic and classical versions of the system is established by a translation, analogous to a translation from intuitionistic logic into the modal logic S4. We also consider the question of completeness of the axioms. BI's spatial implication is used to express weakest preconditions for object-component assignments, and an axiom for allocating a cons cell is shown to be complete under an interpretation of triplesthat allows a command to be applied to states with dangling pointers. We make this latter a feature, by incorporating an operation, and axiom, for disposing of memory. Finally, we describe a local character enjoyed by specifications in the logic, and show how this enables a class of frame axioms, which say what parts of the heap don't change, to be inferred automatically.},
booktitle = {Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {14–26},
numpages = {13},
location = {London, United Kingdom},
series = {POPL '01}
}

@article{GSLeeHJKim20Hoare,
author = {Gyesik Lee and Hwajeong Kim},
journal = {Journal of Knowledge Information Technology and Systems},
issn = {1975-7770},
volume = 15,
number = 2,
pages = {195-193},
year = 2020,
month = 4,
doi = {10.34163/jkits.2020.15.2.004},
url = {https://formal.hknu.ac.kr/Publi/hoare.pdf},
}

@article{Hoare69,
author = {Hoare, C. A. R.},
title = {An Axiomatic Basis for Computer Programming},
year = {1969},
issue_date = {Oct. 1969},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {12},
number = {10},
issn = {0001-0782},
url = {https://doi.org/10.1145/363235.363259},
doi = {10.1145/363235.363259},
abstract = {In this paper an attempt is made to explore the logical foundations of computer programming by use of techniques which were first applied in the study of geometry and have later been extended to other branches of mathematics. This involves the elucidation of sets of axioms and rules of inference which can be used in proofs of the properties of computer programs. Examples are given of such axioms and rules, and a formal proof of a simple theorem is displayed. Finally, it is argued that important advantage, both theoretical and practical, may follow from a pursuance of these topics.},
journal = {Commun. ACM},
month = 10,
pages = {576–580},
numpages = {5},
keywords = {programming language design, formal language definition, axiomatic method, theory of programming' proofs of programs, program documentation, machine-independent programming}
}

@book{Sipser2013,
  address={Boston, MA},
  title={Introduction to the theory of Computation},
  publisher={Cengage Learning},
  author={Sipser, Michael},
  year={2013},
} 

@book{Hopcroft2007,
  address={Boston, MA},
  title={Introduction to automata theory, languages, and computation},
  publisher={Pearson/Addison Wesley},
  author={Hopcroft, John E. and Motwani, Rajeev and Ullman, Jeffrey D.},
  year={2007}
}
 
@book{OxEKdict,
  author = "Hornby, A. S. and Jeong, Young-Kuk and Cho, Mi-ock",
  title = "{Oxford} advanced learner’s {English}-{Korean} dictionary",
  year = 2009,
  publisher = "Oxford University Press",
  address = "London, England",
  isbn = "9780194001144",
  note = {via NAVER's online dictionary service},
}

@misc{MWdict,
   title = {``Parse'' definition \& meaning},
   url={https://www.merriam-webster.com/dictionary/parse},
   journal={Merriam-Webster},
   publisher={Merriam-Webster},
   note={Accessed 6 Jan. 2022}
}

@book{IntroEngSem,
  author = "Kreidler, C. W.",
  title = "Introducing {English} semantics",
  address = "London, England",
  publisher = "Routledge",
  year = 1998,
}

@Article{Chomsky56,
  title =	"Three models for the description of language",
  author =	"Noam Chomsky",
  journal =	"IRE Transactions on Information Theory",
  year = 	"1956",
  volume =	"2",
  note = 	"reprinted in R. D. Luce, R. Bush and E. Galanter
		 (Eds.), {\em Readings in Mathematical Psychology}, Vol.
		 II, Wiley, 1965",
}

@misc{Swift5Ref,
  title        = "Lexical structure --- the {Swift} programming language ({Swift} 5.5)",
  booktitle    = "Swift.org",
  author       = "{Apple Inc}",
  howpublished = "\url{https://docs.swift.org/swift-book/ReferenceManual/LexicalStructure.html}",
  note         = "Accessed: 2022-1-10"
}

@MISC{CSharp6Draft,
  title        = "Lexical structure",
  booktitle    = "C\# 6.0 draft specification",
  author       = "{Microsoft.com}",
  howpublished = "\url{https://docs.microsoft.com/en-us/dotnet/csharp/language-reference/language-specification/lexical-structure}",
  note         = "Accessed: 2022-1-10. (language: en)",
}

@book{JavaSE8spec,
author = {Gosling, James and Joy, Bill and Steele, Guy L. and Bracha, Gilad and Buckley, Alex},
title = {The Java Language Specification, Java SE 8 Edition},
year = {2014},
isbn = {013390069X},
publisher = {Addison-Wesley Professional},
edition = {1st},
abstract = {Written by the inventors of the technology, The Java Language Specification, Java SE 8 Edition is the definitive technical reference for the Java programming language. The book provides complete, accurate, and detailed coverage of the Java programming language. It fully describes the new features added in Java SE 8, including lambda expressions, method references, default methods, type annotations, and repeating annotations. The book also includes many explanatory notes and carefully distinguishes the formal rules of the language from the practical behavior of compilers.}
}

@MISC{Haskell2010,
    author = {Simon Marlow},
    title = {Haskell 2010 Language Report},
    year = {2010}
}

@Book{Winskel93,
  author =	"Glynn Winskel",
  title =	"The Formal Semantics of Programming Languages: An Introduction",
  series =	"Foundation of Computing Series",
  publisher =	"The MIT Press",
  address =	"Cambridge, MA",
  year = 	"1993",
}

@Article{Milner78,
  author =	"Robin Milner",
  title =	"A Theory of Type Polymorphism in Programming",
  journal =	"Journal of Computer and System Sciences",
  volume =	"17",
  year = 	"1978",
  month =	12,
  number =	"3",
  pages =	"348--375",
  checked =	"19 October 1990",
}

@Article{tal-toplas99,
  author =	"Greg Morrisett and David Walker and Karl Crary and Neal Glew",
  title =	"From {System-F} to Typed Assembly Language",
  journal =	"ACM Transactions on Programming Languages and Systems",
  volume =	"21",
  number =	"3",
  pages =	"527--568",
  month =	5,
  year = 	"1999",
}

@Book{Mitchell96fpl,
  author =	"John C. Mitchell",
  title =	"Foundations for Programming Languages",
  publisher =	"The MIT Press",
  year = 	"1996",
  address =	"Cambridge, Mass.",
  ISBN = 	"0-262-13321-0",
  annote =	"Graduate text on programming language theory. Focus on
		 typed lambda calculus. Hundreds of references.",
}

@article{einstein,
  author =       "Albert Einstein",
  title =        "{Zur Elektrodynamik bewegter K{\"o}rper}. ({German})
                 [{On} the electrodynamics of moving bodies]",
  journal =      "Annalen der Physik",
  volume =       "322",
  number =       "10",
  pages =        "891--921",
  year =         "1905",
  DOI =          "http://dx.doi.org/10.1002/andp.19053221004",
  keywords =     "physics"
}

@book{dirac,
  title={The Principles of Quantum Mechanics},
  author={Paul Adrien Maurice Dirac},
  isbn={9780198520115},
  series={International series of monographs on physics},
  year={1981},
  publisher={Clarendon Press},
  keywords = {physics}
}

@book{latexcompanion,
    author    = "Michel Goossens and Frank Mittelbach and Alexander Samarin",
    title     = "The \LaTeX\ Companion",
    year      = "1993",
    publisher = "Addison-Wesley",
    address   = "Reading, Massachusetts",
    keywords  = "latex"
}
 
@online{knuthwebsite,
    author    = "Donald Knuth",
    title     = "Knuth: Computers and Typesetting",
    url       = "http://www-cs-faculty.stanford.edu/~uno/abcde.html",
    keywords  = "latex,knuth"
}

@inbook{knuth-fa,
   author = "Donald E. Knuth",
   title = "Fundamental Algorithms",
   publisher = "Addison-Wesley",
   year = "1973",
   chapter = "1.2",
   keywords  = "knuth,programming"
}

@book{knuth-acp,
   author = "Donald E. Knuth",
   publisher = "Addison-Wesley",
   title = "The Art of Computer Programming",
   series = "Four volumes",
   year = "1968",
   note = "Seven volumes planned",
   keywords  = "knuth,programming"
}

@article{ctan,
    author  = "George D. Greenwade",
    title   = "The {C}omprehensive {T}ex {A}rchive {N}etwork ({CTAN})",
    year    = "1993",
    journal = "TUGBoat",
    volume  = "14",
    number  = "3",
    pages   = "342--351",
    keywords  = "latex"
}