lob.bib

% Encoding: UTF-8

@InProceedings{Altenkirch:2007:OE:1292597.1292608,
  author =    {Altenkirch, Thorsten and McBride, Conor and Swierstra, Wouter},
  title =     {Observational Equality, Now!},
  booktitle = {Proceedings of the 2007 Workshop on Programming Languages Meets Program Verification},
  year =      {2007},
  series =    {PLPV '07},
  pages =     {57--68},
  address =   {New York, NY, USA},
  publisher = {ACM},
  abstract =  {This paper has something new and positive to say about propositional equality in programming and proof systems based on the Curry-Howard correspondence between propositions and types. We have found a way to present a propositional equality type
\begin{itemize}
\item which is substitutive, allowing us to reason by replacing equal for equal in propositions;
\item which reflects the observable behaviour of values rather than their construction: in particular, we \item have extensionality-- functions are equal if they take equal inputs to equal outputs;
\item which retains strong normalisation, decidable typechecking and canonicity--the property that closed normal forms inhabiting datatypes have canonical constructors;
\item which allows inductive data structures to be expressed in terms of a standard characterisation of well-founded trees;
\item which is presented syntactically--you can implement it directly, and we are doing so this approach stands at the core of Epigram 2;
\item which you can play with now: we have simulated our system by a shallow embedding in Agda 2, shipping as part of the standard examples package for that system [21].
\end{itemize}
Until now, it has always been necessary to sacrifice some of these aspects. The closest attempt in the literature is Altenkirch's construction of a setoid-model for a system with canonicity and extensionality on top of an intensional type theory with proof-irrelevant propositions [4]. Our new proposal simplifies Altenkirch's construction by adopting McBride's heterogeneous approach to equality [19].},
  acmid =     {1292608},
  doi =       {10.1145/1292597.1292608},
  isbn =      {978-1-59593-677-6},
  keywords =  {equality, type theory},
  location =  {Freiburg, Germany},
  numpages =  {12},
  url =       {http://www.cs.nott.ac.uk/~psztxa/publ/obseqnow.pdf}
}

@Article{altenkirch2006towards,
  author =   {Altenkirch, Thorsten and McBride, Conor},
  title =    {Towards Observational Type Theory},
  journal =  {Manuscript, available online},
  year =     {2006},
  abstract = {Observational Type Theory (OTT) combines benefi-
cial aspects of Intensional and Extensional Type Theory
(ITT/ETT). It separates definitional equality, decidable as in
ITT, and a substitutive propositional equality, capturing extensional
equality of functions, as in ETT. Moreover, canonicity
holds: any closed term is definitionally reducible to a
canonical value.

Building on previous work by each author, this article
reports substantial progress in the form of a simplified theory
with a straightforward syntactic presentation, which we
have implemented.

As well as simplifying reasoning about functions, OTT
offers potential foundational benefits, e.g. it gives rise to a
closed type theory encoding inductive datatypes.},
  url =      {http://strictlypositive.org/ott.pdf}
}


@Article{appel2007very,
  Title                    = {A Very Modal Model of a Modern, Major, General Type System},
  Author                   = {Appel, Andrew W and Mellies, Paul-Andr{\'e} and Richards, Christopher D and Vouillon, J{\'e}r{\^o}me},
  Journal                  = {ACM SIGPLAN Notices},
  Year                     = {2007},
  Number                   = {1},
  Pages                    = {109--122},
  Volume                   = {42},

  Owner                    = {jgross},
  Publisher                = {ACM},
  Timestamp                = {2016.03.09},
  Url                      = {https://www.cs.princeton.edu/~appel/papers/modalmodel.pdf}
}

@Article{BaraszChristianoFallensteinEtAl2014,
  author =         {Mihaly Barasz and Paul Christiano and Benja Fallenstein and Marcello Herreshoff and Patrick LaVictoire and Eliezer Yudkowsky},
  title =          {Robust Cooperation in the Prisoner's Dilemma: Program Equilibrium via Provability Logic},
  journal =        {ArXiv e-prints},
  year =           {2014},
  month =          {Jan},
  __markedentry =  {[Jason:]},
  abstract =       {We consider the one-shot Prisoner's Dilemma between algorithms with read-access to one anothers' source codes, and we use the modal logic of provability to build agents that can achieve mutual cooperation in a manner that is robust, in that cooperation does not require exact equality of the agents' source code, and unexploitable, meaning that such an agent never cooperates when its opponent defects. We construct a general framework for such "modal agents", and study their properties.},
  comments =       {18 pages},
  eprint =         {1401.5577},
  oai2identifier = {1401.5577},
  url =            {http://arxiv.org/pdf/1401.5577v1.pdf}
}

@Article{Berarducci1985,
  author =    {Berarducci, Alessandro and B\"{o}hm, Corrado},
  title =     {Automatic synthesis of typed $\Lambda$-programs on term algebras},
  journal =   {Theoretical Computer Science},
  year =      {1985},
  volume =    {39},
  number =    {820076097},
  pages =     {135--154},
  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 lambda- calculus (Lambsa 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 Lambda-terms with type of degree at most two and a companion corollary for Lambda-programs have been proved. (3) A new congruence relation for the last-mentioned Lambda-terms which is stronger than Lambda-convertibility is introduced and proved to have the meaning of a 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.},
  doi =       {10.1016/0304-3975(85)90135-5},
  publisher = {Elsevier},
  url =       {http://www.sciencedirect.com/science/article/pii/0304397585901355}
}

@InProceedings{brown2016breaking,
  Title                    = {Breaking Through the Normalization Barrier: A Self-Interpreter for F-omega},
  Author                   = {Brown, Matt and Palsberg, Jens},
  Booktitle                = {Proceedings of the 43rd Annual {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages},
  Year                     = {2016},
  Organization             = {ACM},
  Pages                    = {5--17},

  Doi                      = {10.1145/2837614.2837623},
  Owner                    = {jgross},
  Timestamp                = {2016.02.26},
  Url                      = {http://compilers.cs.ucla.edu/popl16/popl16-full.pdf}
}

@Electronic{cartoon-lobs-theorem,
  Title                    = {(The Cartoon Guide to) {L}\"{o}b's Theorem},
  Author                   = {Eliezer Yudkowsky},
  Url                      = {http://www.yudkowsky.net/rational/lobs-theorem},
  Year                     = {2008},

  Owner                    = {jgross},
  Timestamp                = {2016.03.11}
}

@Article{Chapman200921,
  Title                    = {Type Theory Should Eat Itself},
  Author                   = {James Chapman},
  Journal                  = {Electronic Notes in Theoretical Computer Science},
  Year                     = {2009},
  Note                     = {Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice (LFMTP 2008)},
  Pages                    = {21--36},
  Volume                   = {228},

  Abstract                 = {In this paper I present a partial formalisation of a normaliser for type theory in Agda [Ulf Norell. Agda 2, 2007. http://www.cs.chalmers.se/~ulfn/]; extending previous work on big-step normalisation [Thorsten Altenkirch and James Chapman. Big-Step Normalisation. Journal of Functional Programming, 2008. Special Issue on Mathematically Structured Functional Programming. To appear, Thorsten Altenkirch and James Chapman. Tait in one big step. In Workshop on Mathematically Structured Functional Programming, \{MSFP\} 2006, Kuressaare, Estonia, July 2, 2006, electronic Workshop in Computing (eWiC), Kuressaare, Estonia, 2006. The British Computer Society (BCS)]. The normaliser in written as an environment machine. Only the computational behaviour of the normaliser is presented omitting details of termination. },
  Doi                      = {http://dx.doi.org/10.1016/j.entcs.2008.12.114},
  ISSN                     = {1571-0661},
  Keywords                 = {big-step normalisation},
  Owner                    = {jgross},
  Timestamp                = {2016.03.11},
  Url                      = {http://www.sciencedirect.com/science/article/pii/S157106610800577X}
}

@Article{church1940formulation,
  author =    {Alonzo Church},
  title =     {A Formulation of the Simple Theory of Types},
  journal =   {The Journal of Symbolic Logic},
  year =      {1940},
  volume =    {5},
  number =    {2},
  pages =     {56--68},
  issn =      {00224812},
  publisher = {Association for Symbolic Logic},
  url =       {http://www.jstor.org/stable/2266170}
}

@InCollection{constable1995using,
  Title                    = {Using Reflection to Explain and Enhance Type Theory},
  Author                   = {Constable, Robert L},
  Booktitle                = {Proof and Computation},
  Publisher                = {Springer},
  Year                     = {1995},
  Pages                    = {109--144},

  Abstract                 = {The five lectures at Marktoberdorf on which these notes are based were about the architecture of problem solving environments which use theorem provers. Experience with these systems over the past two decades has shown that the prover must be extensible, yet it must be kept. We examine a way to safely add new decision procedures to the Nuprl prover. It relies on a reflection mechanism and is applicable to any tactic-oriented prover with sufficient reflection. The lectures explain reflection in the setting of constructive type theory, the core logic of Nuprl.},
  Url                      = {http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.23.5290&rep=rep1&type=pdf}
}

@InCollection{danielsson2006formalisation,
  Title                    = {A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family},
  Author                   = {Danielsson, Nils Anders},
  Booktitle                = {Types for Proofs and Programs},
  Publisher                = {Springer Berlin Heidelberg},
  Year                     = {2007},

  Address                  = {Berlin, Heidelberg},
  Chapter                  = {A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family},
  Editor                   = {Altenkirch, Thorsten and McBride, Conor},
  Pages                    = {93--109},
  Series                   = {Lecture Notes in Computer Science},
  Volume                   = {4502},

  Abstract                 = {It is demonstrated how a dependently typed lambda calculus (a logical framework) can be formalised inside a language with inductive- recursive families. The formalisation does not use raw terms; the well- typed terms are defined directly. It is hence impossible to create ill-typed terms.

As an example of programming with strong invariants, and to show that the formalisation is usable, normalisation is proved. Moreover, this proof seems to be the first formal account of normalisation by evaluation for a dependently typed language.},
  Doi                      = {10.1007/978-3-540-74464-1_7},
  ISBN                     = {978-3-540-74464-1},
  Owner                    = {jgross},
  Timestamp                = {2016.03.11},
  Url                      = {http://dx.doi.org/10.1007/978-3-540-74464-1_7}
}

@Article{Davies:2001:MAS:382780.382785,
  author =     {Davies, Rowan and Pfenning, Frank},
  title =      {A Modal Analysis of Staged Computation},
  journal =    {J. ACM},
  year =       {2001},
  volume =     {48},
  number =     {3},
  pages =      {555--604},
  month =      may,
  acmid =      {382785},
  address =    {New York, NY, USA},
  doi =        {10.1145/382780.382785},
  issn =       {0004-5411},
  issue_date = {May 2001},
  keywords =   {binding times, run-time code generation, staged computation},
  numpages =   {50},
  publisher =  {ACM},
  url =        {http://doi.acm.org/10.1145/382780.382785}
}

@InProceedings{DBLP:conf/ershov/Mogensen01,
  author =    {Torben {\AE}. Mogensen},
  title =     {An Investigation of Compact and Efficient Number Representations in the Pure Lambda Calculus},
  booktitle = {Perspectives of System Informatics, 4th International Andrei Ershov Memorial Conference, {PSI} 2001, Akademgorodok, Novosibirsk, Russia, July 2-6, 2001, Revised Papers},
  year =      {2001},
  pages =     {205--213},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  biburl =    {http://dblp.uni-trier.de/rec/bib/conf/ershov/Mogensen01},
  doi =       {10.1007/3-540-45575-2_20},
  timestamp = {Thu, 17 Sep 2009 10:48:56 +0200},
  url =       {http://dx.doi.org/10.1007/3-540-45575-2_20}
}

@Article{DBLP:journals/corr/abs-cs-0505034,
  Title                    = {Essential Incompleteness of Arithmetic Verified by Coq},
  Author                   = {Russell O'Connor},
  Journal                  = {CoRR},
  Year                     = {2005},
  Volume                   = {abs/cs/0505034},

  Bibsource                = {dblp computer science bibliography, http://dblp.org},
  Biburl                   = {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-cs-0505034},
  Owner                    = {jgross},
  Timestamp                = {2016.03.11},
  Url                      = {http://arxiv.org/abs/cs/0505034}
}

@Misc{geuvers2014church,
  author = {Geuvers, Herman},
  title =  {The {C}hurch-{S}cott representation of inductive and coinductive data},
  year =   {2014},
  url =    {http://www.cs.ru.nl/~herman/PUBS/ChurchScottDataTypes.pdf}
}

@Article{godel1931formal,
  Title                    = {{\"U}ber formal unentscheidbare {S}{\"a}tze der {P}rincipia {M}athematica und verwandter {S}ysteme {I}},
  Author                   = {G{\"o}del, Kurt},
  Journal                  = {Monatshefte f{\"u}r mathematik und physik},
  Year                     = {1931},
  Number                   = {1},
  Pages                    = {173--198},
  Volume                   = {38},

  Owner                    = {jgross},
  Publisher                = {Springer},
  Timestamp                = {2016.03.13},
  Url                      = {http://www.w-k-essler.de/pdfs/goedel.pdf}
}

@Book{hofstadter1980godel,
  Title                    = {G{\"o}del, {E}scher, {B}ach: An Eternal Golden Braid},
  Author                   = {Hofstadter, Douglas R.},
  Publisher                = {Vintage},
  Year                     = {1979},

  ISBN                     = {978-0394745022},
  Owner                    = {jgross},
  Timestamp                = {2016.03.13}
}

@Misc{Kiselyov2012,
  author = {Oleg Kiselyov},
  title =  {Beyond Church encoding: Boehm-Berarducci isomorphism of algebraic data types and polymorphic lambda-terms},
  month =  {April},
  year =   {2012},
  url =    {http://okmij.org/ftp/tagless-final/course/Boehm-Berarducci.html}
}

@Book{kleene1952introduction,
  Title                    = {Introduction to Metamathematics},
  Author                   = {Kleene, Stephen Cole},
  Publisher                = {Wolters-Noordhoff},
  Year                     = {1952},

  ISBN                     = {0-7204-2103-9},
  Owner                    = {jgross},
  Timestamp                = {2016.03.13}
}

@Misc{loopsnoop,
  Title                    = {Scooping the Loop Snooper},

  Author                   = {Geoffrey K. Pullum},
  Month                    = {October},
  Year                     = {2000},

  Organization             = {University of Edinburgh},
  Owner                    = {jgross},
  Timestamp                = {2016.02.26},
  Url                      = {http://www.lel.ed.ac.uk/~gpullum/loopsnoop.html}
}

@InProceedings{mcbride2010outrageous,
  Title                    = {Outrageous but Meaningful Coincidences: Dependent type-safe syntax and evaluation},
  Author                   = {McBride, Conor},
  Booktitle                = {Proceedings of the 6th ACM SIGPLAN workshop on Generic programming},
  Year                     = {2010},
  Organization             = {ACM},
  Pages                    = {1--12},

  Abstract                 = {Tagless interpreters for well-typed terms in some object language are a standard example of the power and benefit of precise indexing in types, whether with dependent types, or generalized algebraic datatypes. The key is to reflect object language types as indices (however they may be constituted) for the term datatype in the host language, so that host type coincidence ensures object type coincidence. Whilst this technique is widespread for simply typed object languages, dependent types have proved a tougher nut with nontrivial computation in type equality. In their type-safe representations, Danielsson [2006] and Chapman [2009] succeed in capturing the equality rules, but at the cost of representing equality derivations explicitly within terms. This article delivers a type-safe representation for a dependently typed object language, dubbed KIPLING, whose computational type equality just appropriates that of its host, Agda. The \textsc{Kipling} interpreter example is not merely \emph{de rigeur}--- it is key to the construction. At the heart of the technique is that key component of generic programming, the \emph{universe}.},
  Url                      = {https://personal.cis.strath.ac.uk/conor.mcbride/pub/DepRep/DepRep.pdf}
}

@InProceedings{nott31169,
  author =    {Thorsten Altenkirch and Ambrus Kaposi},
  title =     {Type Theory in Type Theory using Quotient Inductive Types},
  booktitle = {POPL '16 The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  year =      {2016},
  publisher = {ACM},
  abstract =  {We present an internal formalisation of a type heory with dependent types in Type Theory using a special case of higher inductive types from Homotopy Type Theory which we call quotient inductive types (QITs). Our formalisation of type theory avoids referring to preterms or a typability relation but defines directly well typed objects by an inductive definition. We use the elimination principle to define the set-theoretic and logical predicate interpretation. The work has been formalized using the Agda system extended with QITs using postulates.},
  journal =   {Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  keywords =  {Higher Inductive Types, Homotopy Type Theory, Logical Relations, Metaprogramming, Agda},
  url =       {http://eprints.nottingham.ac.uk/31169/}
}

@Article{paulson2015mechanised,
  Title                    = {A Mechanised Proof of {G}{\"o}del's Incompleteness Theorems using {N}ominal {I}sabelle},
  Author                   = {Paulson, Lawrence C},
  Journal                  = {Journal of Automated Reasoning},
  Year                     = {2015},
  Number                   = {1},
  Pages                    = {1--37},
  Volume                   = {55},

  Abstract                 = {An Isabelle/HOL formalisation of G{\"o}del's two incompleteness theorems is presented. The work follows {\'{S}}wierczkowski's detailed proof of the theorems using hereditarily finite (HF) set theory (Dissertationes Mathematicae 422, 1--58, 2003). Avoiding the usual arithmetical encodings of syntax eliminates the necessity to formalise elementary number theory within an embedded logical calculus. The Isabelle formalisation uses two separate treatments of variable binding: the nominal package (Logical Methods in Computer Science 8(2:14), 1--35, 2012) is shown to scale to a development of this complexity, while de Bruijn indices (Indagationes Mathematicae 34, 381--392, 1972) turn out to be ideal for coding syntax. Critical details of the Isabelle proof are described, in particular gaps and errors found in the literature.},
  Owner                    = {jgross},
  Publisher                = {Springer},
  Timestamp                = {2016.03.11},
  Url                      = {https://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf}
}

@Article{PFENNING1991137,
  author =   {Frank Pfenning and Peter Lee},
  title =    {Metacircularity in the polymorphic $\lambda$-calculus},
  journal =  {Theoretical Computer Science},
  year =     {1991},
  volume =   {89},
  number =   {1},
  pages =    {137--159},
  abstract = {We consider the question of whether a useful notion of metacircularity exists for the polymorphic λ-calculus. Even though complete metacircularity seems to be impossible, we obtain a close approximation to a metacircular interpreter. We begin by presenting an encoding for the Girard-Reynolds second-order polymorphic λ-calculus in the third-order polymorphic λ-calculus. The encoding makes use of representations in which abstractions are represented by abstractions, thus eliminating the need for the explicit representation of environments. We then extend this construction to encompass all of the ω-order polymorphic λ-calculus (Fω). The representation has the property that evaluation is definable, and furthermore that only well-typed terms can be represented and thus type inference does not have to be explicitly defined. Unfortunately, this metacircularity result seems to fall short of providing a useful framework for typed metaprogramming. We speculate on the reasons for this failure and the prospects for overcoming it in the future. In addition, we briefly describe our efforts in designing a practical programming language based on Fω.},
  doi =      {http://dx.doi.org/10.1016/0304-3975(90)90109-U},
  issn =     {0304-3975},
  url =      {http://www.sciencedirect.com/science/article/pii/030439759090109U}
}

@Misc{piponi-from-l-theorem-to-spreadsheet,
  Title                    = {From Löb's Theorem to Spreadsheet Evaluation},

  Author                   = {Dan Piponi},
  Month                    = {November},
  Year                     = {2006},

  Organization             = {A Neighborhood of Infinity},
  Owner                    = {jgross},
  Timestamp                = {2016.03.11},
  Url                      = {http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet.html}
}

@Unpublished{scott1963system,
  author = {Scott, Dana},
  title =  {A system of functional abstraction},
  note =   {Unpublished manuscript},
  year =   {1963}
}

@PhdThesis{Shankar:1986:PM:913294,
  Title                    = {Proof-checking Metamathematics (Theorem-proving)},
  Author                   = {Shankar, Natarajan},
  School                   = {The University of Texas at Austin},
  Year                     = {1986},
  Note                     = {AAI8717580},

  Owner                    = {jgross},
  Publisher                = {The University of Texas at Austin},
  Timestamp                = {2016.03.11}
}

@Book{shankar1997metamathematics,
  Title                    = {Metamathematics, Machines and {G}{\"o}del's Proof},
  Author                   = {Shankar, Natarajan},
  Publisher                = {Cambridge University Press},
  Year                     = {1997},

  Owner                    = {jgross},
  Timestamp                = {2016.03.11}
}

@Article{SimmonsToninho2012,
  author =         {Robert J. Simmons and Bernardo Toninho},
  title =          {Constructive Provability Logic},
  journal =        {CoRR},
  year =           {2012},
  volume =         {abs/1205.6402},
  month =          {May},
  __markedentry =  {[Jason:6]},
  abstract =       {We present constructive provability logic, an intuitionstic modal logic that validates the L\"ob rule of G\"odel and L\"ob's provability logic by permitting logical reflection over provability. Two distinct variants of this logic, CPL and CPL*, are presented in natural deduction and sequent calculus forms which are then shown to be equivalent. In addition, we discuss the use of constructive provability logic to justify stratified negation in logic programming within an intuitionstic and structural proof theory.},
  bibsource =      {dblp computer science bibliography, http://dblp.org},
  biburl =         {http://dblp.uni-trier.de/rec/bib/journals/corr/abs-1205-6402},
  comments =       {Extended version of IMLA 2011 submission of the same title},
  eprint =         {1205.6402},
  oai2identifier = {1205.6402},
  timestamp =      {Wed, 10 Oct 2012 21:28:52 +0200},
  url =            {http://arxiv.org/abs/1205.6402}
}

@Article{tarski1936undefinability,
  Title                    = {Der {W}ahrheitsbegriff in den formalisierten {S}prachen},
  Author                   = {Tarski, Alfred},
  Journal                  = {Studia Philosophica},
  Year                     = {1936},
  Pages                    = {261--405},
  Volume                   = {1},

  Owner                    = {jgross},
  Timestamp                = {2016.03.13},
  Url                      = {http://www.w-k-essler.de/pdfs/Tarski.pdf}
}

@Misc{Yudkowsky2014,
  Title                    = {Lob's Theorem Cured My Social Anxiety},

  Author                   = {Brienne Yudkowsky},
  Month                    = {February},
  Year                     = {2014},

  Organization             = {Agenty Duck},
  Url                      = {http://agentyduck.blogspot.com/2014/02/lobs-theorem-cured-my-social-anxiety.html}
}