Making a subdirectory of sbmf
This commit is contained in:
wadler
parent
1d43cc934c
commit
9982e0464c
49 changed files with 0 additions and 1844 deletions
|
|
@ -1,96 +0,0 @@
|
|||
\relax
|
||||
\citation{Pierce-2002}
|
||||
\citation{Pierce-et-al-2010}
|
||||
\citation{Huet-et-al-1997}
|
||||
\citation{Pierce-2009}
|
||||
\@writefile{toc}{\contentsline {title}{Programming Language Foundations in Agda}{1}}
|
||||
\@writefile{toc}{\authcount {1}}
|
||||
\@writefile{toc}{\contentsline {author}{Philip Wadler}{1}}
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}}
|
||||
\citation{Bove-et-al-2009}
|
||||
\citation{Stump-2016}
|
||||
\citation{Gonthier-2008}
|
||||
\citation{Gonthier-et-al-2013}
|
||||
\citation{Hales-et-al-2017}
|
||||
\citation{Leroy-2009,Kastner-et-al-2017}
|
||||
\citation{Klein-2009,O'Connor-2016}
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {2}Scope}{3}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{Naturals: Natural numbers}{3}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{Induction: Proof by induction}{4}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{Relations: Inductive definitions of relations}{4}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{Equality: Equality and equational reasoning}{4}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{Isomorphism: Isomorphism and embedding}{4}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{Connectives: Conjunction, disjunction, and implication}{4}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{Negation: Negation, with intuitionistic and classical logic}{4}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{Quantifiers: Universals and existentials}{4}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{Lists: Lists and higher-order functions}{4}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{Decidable: Booleans and decision procedures}{4}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{Lambda: Introduction to lambda calculus}{4}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{Properties: Progress and preservation}{5}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{DeBruijn: Inherently typed de Bruijn representation}{5}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{More: More constructs of simply-typed lambda calculus}{5}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{Bisimulation: Relating reduction systems}{5}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{Inference: Bidirectional type inference}{5}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{Untyped: Untyped calculus with full normalisation}{5}}
|
||||
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces PLFA, Progress (1/2)}}{6}}
|
||||
\newlabel{fig:plfa-progress-1}{{1}{6}}
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {3}Proofs in Agda and Coq}{6}}
|
||||
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces PLFA, Progress (2/2)}}{7}}
|
||||
\newlabel{fig:plfa-progress-2}{{2}{7}}
|
||||
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces SF, Progress (1/2)}}{8}}
|
||||
\newlabel{fig:sf-progress-1}{{3}{8}}
|
||||
\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces SF, Progress (2/2)}}{9}}
|
||||
\newlabel{fig:sf-progress-2}{{4}{9}}
|
||||
\citation{Danas-et-al-2017}
|
||||
\citation{Wright-and-Felleisen-1994}
|
||||
\citation{Felleisen-et-al-2009}
|
||||
\citation{Rosu-Serbanuta-2010}
|
||||
\citation{Bove-and-Capretta-2001}
|
||||
\citation{Capretta-2005}
|
||||
\citation{McBride-2015}
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {4}Progress + Preservation = Evaluation}{11}}
|
||||
\@writefile{lof}{\contentsline {figure}{\numberline {5}{\ignorespaces PLFA, Evaluation}}{12}}
|
||||
\newlabel{fig:plfa-eval}{{5}{12}}
|
||||
\citation{Harper-2016}
|
||||
\citation{Berger-1993,Dagand-and-Scherer-2015}
|
||||
\citation{Kiselyov-2009}
|
||||
\citation{McBride-2005}
|
||||
\citation{Goguen-and-McKinna-1997}
|
||||
\citation{Allais-et-al-2017}
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {5}Inherent typing is golden}{13}}
|
||||
\citation{Altenkirch-and-Reus-1999}
|
||||
\citation{Chapman-2009}
|
||||
\citation{Allais-et-al-2017}
|
||||
\bibstyle{plainnat}
|
||||
\bibdata{PLFA}
|
||||
\@writefile{toc}{\contentsline {section}{\numberline {6}Conclusion}{14}}
|
||||
\@writefile{toc}{\contentsline {paragraph}{Acknowledgements}{14}}
|
||||
\bibcite{Allais-et-al-2017}{{1}{2017}{{Allais et~al.}}{{Allais, Chapman, McBride, and McKinna}}}
|
||||
\bibcite{Altenkirch-and-Reus-1999}{{2}{1999}{{Altenkirch and Reus}}{{}}}
|
||||
\bibcite{Berger-1993}{{3}{1993}{{Berger}}{{}}}
|
||||
\bibcite{Bove-and-Capretta-2001}{{4}{2001}{{Bove and Capretta}}{{}}}
|
||||
\bibcite{Bove-et-al-2009}{{5}{2009}{{Bove et~al.}}{{Bove, Dybjer, and Norell}}}
|
||||
\bibcite{Capretta-2005}{{6}{2005}{{Capretta}}{{}}}
|
||||
\bibcite{Chapman-2009}{{7}{2009}{{Chapman}}{{}}}
|
||||
\bibcite{Dagand-and-Scherer-2015}{{8}{2015}{{Dagand and Scherer}}{{}}}
|
||||
\bibcite{Danas-et-al-2017}{{9}{2017}{{Danas et~al.}}{{Danas, Nelson, Harrison, Krishnamurthi, and Dougherty}}}
|
||||
\bibcite{Felleisen-et-al-2009}{{10}{2009}{{Felleisen et~al.}}{{Felleisen, Findler, and Flatt}}}
|
||||
\bibcite{Goguen-and-McKinna-1997}{{11}{1997}{{Goguen and McKinna}}{{}}}
|
||||
\bibcite{Gonthier-2008}{{12}{2008}{{Gonthier}}{{}}}
|
||||
\bibcite{Gonthier-et-al-2013}{{13}{2013}{{Gonthier et~al.}}{{Gonthier, Asperti, Avigad, et~al.}}}
|
||||
\bibcite{Hales-et-al-2017}{{14}{2017}{{Hales et~al.}}{{Hales, Adams, Bauer, Dang, Harrison, Le~Truong, Kaliszyk, Magron, McLaughlin, Nguyen, et~al.}}}
|
||||
\bibcite{Harper-2016}{{15}{2016}{{Harper}}{{}}}
|
||||
\bibcite{Huet-et-al-1997}{{16}{1997}{{Huet et~al.}}{{Huet, Kahn, and Paulin-Mohring}}}
|
||||
\bibcite{Kastner-et-al-2017}{{17}{2017}{{K{\"a}stner et~al.}}{{K{\"a}stner, Leroy, Blazy, Schommer, Schmidt, and Ferdinand}}}
|
||||
\bibcite{Kiselyov-2009}{{18}{2009}{{Kiselyov}}{{}}}
|
||||
\bibcite{Klein-2009}{{19}{2009}{{Klein et~al.}}{{Klein, Elphinstone, Heiser, Andronick, Cock, Derrin, Elkaduwe, Engelhardt, Kolanski, Norrish, et~al.}}}
|
||||
\bibcite{Leroy-2009}{{20}{2009}{{Leroy}}{{}}}
|
||||
\bibcite{McBride-2005}{{21}{2005}{{McBride}}{{}}}
|
||||
\bibcite{McBride-2015}{{22}{2015}{{McBride}}{{}}}
|
||||
\bibcite{O'Connor-2016}{{23}{2016}{{O'Connor et~al.}}{{O'Connor, Chen, Rizkallah, Amani, Lim, Murray, Nagashima, Sewell, and Klein}}}
|
||||
\bibcite{Pierce-2009}{{24}{2009}{{Pierce}}{{}}}
|
||||
\bibcite{Pierce-2002}{{25}{2002}{{Pierce and Benjamin}}{{}}}
|
||||
\bibcite{Pierce-et-al-2010}{{26}{2010}{{Pierce et~al.}}{{Pierce, Casinghino, Gaboardi, Greenberg, Hri{\c {t}}cu, Sj{\"o}berg, and Yorgey}}}
|
||||
\bibcite{Rosu-Serbanuta-2010}{{27}{2010}{{Ro{\c s}u and {\c S}erb{\u a}nu{\c t}{\u a}}}{{}}}
|
||||
\bibcite{Stump-2016}{{28}{2016}{{Stump}}{{}}}
|
||||
\bibcite{Wright-and-Felleisen-1994}{{29}{1994}{{Wright and Felleisen}}{{}}}
|
||||
191
sbmf/PLFA.bbl
191
sbmf/PLFA.bbl
|
|
@ -1,191 +0,0 @@
|
|||
\begin{thebibliography}{29}
|
||||
\providecommand{\natexlab}[1]{#1}
|
||||
\providecommand{\url}[1]{\texttt{#1}}
|
||||
\expandafter\ifx\csname urlstyle\endcsname\relax
|
||||
\providecommand{\doi}[1]{doi: #1}\else
|
||||
\providecommand{\doi}{doi: \begingroup \urlstyle{rm}\Url}\fi
|
||||
|
||||
\bibitem[Allais et~al.(2017)Allais, Chapman, McBride, and
|
||||
McKinna]{Allais-et-al-2017}
|
||||
Guillaume Allais, James Chapman, Conor McBride, and James McKinna.
|
||||
\newblock Type-and-scope safe programs and their proofs.
|
||||
\newblock In \emph{Proceedings of the 6th ACM SIGPLAN Conference on Certified
|
||||
Programs and Proofs}, pages 195--207. ACM, 2017.
|
||||
|
||||
\bibitem[Altenkirch and Reus(1999)]{Altenkirch-and-Reus-1999}
|
||||
Thorsten Altenkirch and Bernhard Reus.
|
||||
\newblock Monadic presentations of lambda terms using generalized inductive
|
||||
types.
|
||||
\newblock In \emph{International Workshop on Computer Science Logic}, pages
|
||||
453--468. Springer, 1999.
|
||||
|
||||
\bibitem[Berger(1993)]{Berger-1993}
|
||||
Ulrich Berger.
|
||||
\newblock Program extraction from normalization proofs.
|
||||
\newblock In \emph{International Conference on Typed Lambda Calculi and
|
||||
Applications}, pages 91--106. Springer, 1993.
|
||||
|
||||
\bibitem[Bove and Capretta(2001)]{Bove-and-Capretta-2001}
|
||||
Ana Bove and Venanzio Capretta.
|
||||
\newblock Nested general recursion and partiality in type theory.
|
||||
\newblock In \emph{International Conference on Theorem Proving in Higher Order
|
||||
Logics}, pages 121--125. Springer, 2001.
|
||||
|
||||
\bibitem[Bove et~al.(2009)Bove, Dybjer, and Norell]{Bove-et-al-2009}
|
||||
Ana Bove, Peter Dybjer, and Ulf Norell.
|
||||
\newblock A brief overview of agda--a functional language with dependent types.
|
||||
\newblock In \emph{International Conference on Theorem Proving in Higher Order
|
||||
Logics}, pages 73--78. Springer, 2009.
|
||||
|
||||
\bibitem[Capretta(2005)]{Capretta-2005}
|
||||
Venanzio Capretta.
|
||||
\newblock General recursion via coinductive types.
|
||||
\newblock \emph{Logical Methods in Computer Science}, 1\penalty0 (2), 2005.
|
||||
|
||||
\bibitem[Chapman(2009)]{Chapman-2009}
|
||||
James~Maitland Chapman.
|
||||
\newblock \emph{Type checking and normalisation}.
|
||||
\newblock PhD thesis, University of Nottingham, 2009.
|
||||
|
||||
\bibitem[Dagand and Scherer(2015)]{Dagand-and-Scherer-2015}
|
||||
Pierre-{\'E}variste Dagand and Gabriel Scherer.
|
||||
\newblock Normalization by realizability also evaluates.
|
||||
\newblock In \emph{Vingt-sixi{\`e}mes Journ{\'e}es Francophones des Langages
|
||||
Applicatifs (JFLA 2015)}, 2015.
|
||||
|
||||
\bibitem[Danas et~al.(2017)Danas, Nelson, Harrison, Krishnamurthi, and
|
||||
Dougherty]{Danas-et-al-2017}
|
||||
Natasha Danas, Tim Nelson, Lane Harrison, Shriram Krishnamurthi, and Daniel~J
|
||||
Dougherty.
|
||||
\newblock User studies of principled model finder output.
|
||||
\newblock In \emph{International Conference on Software Engineering and Formal
|
||||
Methods}, pages 168--184. Springer, 2017.
|
||||
|
||||
\bibitem[Felleisen et~al.(2009)Felleisen, Findler, and
|
||||
Flatt]{Felleisen-et-al-2009}
|
||||
Matthias Felleisen, Robert~Bruce Findler, and Matthew Flatt.
|
||||
\newblock \emph{Semantics engineering with PLT Redex}.
|
||||
\newblock By Press, 2009.
|
||||
|
||||
\bibitem[Goguen and McKinna(1997)]{Goguen-and-McKinna-1997}
|
||||
Healfdene Goguen and James McKinna.
|
||||
\newblock Candidates for substitution.
|
||||
\newblock Technical report, Laboratory for Foundations of Computer Science,
|
||||
University of Edinburgh, 1997.
|
||||
|
||||
\bibitem[Gonthier(2008)]{Gonthier-2008}
|
||||
Georges Gonthier.
|
||||
\newblock The four colour theorem: Engineering of a formal proof.
|
||||
\newblock In \emph{Computer mathematics}, pages 333--333. Springer, 2008.
|
||||
|
||||
\bibitem[Gonthier et~al.(2013)Gonthier, Asperti, Avigad,
|
||||
et~al.]{Gonthier-et-al-2013}
|
||||
Georges Gonthier, Andrea Asperti, Jeremy Avigad, et~al.
|
||||
\newblock A machine-checked proof of the odd order theorem.
|
||||
\newblock In \emph{International Conference on Interactive Theorem Proving},
|
||||
pages 163--179. Springer, 2013.
|
||||
|
||||
\bibitem[Hales et~al.(2017)Hales, Adams, Bauer, Dang, Harrison, Le~Truong,
|
||||
Kaliszyk, Magron, McLaughlin, Nguyen, et~al.]{Hales-et-al-2017}
|
||||
Thomas Hales, Mark Adams, Gertrud Bauer, Tat~Dat Dang, John Harrison, Hoang
|
||||
Le~Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat~Thang Nguyen,
|
||||
et~al.
|
||||
\newblock A formal proof of the {K}epler conjecture.
|
||||
\newblock In \emph{Forum of Mathematics, Pi}, volume~5. Cambridge University
|
||||
Press, 2017.
|
||||
|
||||
\bibitem[Harper(2016)]{Harper-2016}
|
||||
Robert Harper.
|
||||
\newblock \emph{Practical foundations for programming languages}.
|
||||
\newblock Cambridge University Press, 2016.
|
||||
|
||||
\bibitem[Huet et~al.(1997)Huet, Kahn, and Paulin-Mohring]{Huet-et-al-1997}
|
||||
G{\'e}rard Huet, Gilles Kahn, and Christine Paulin-Mohring.
|
||||
\newblock The {C}oq proof assistant a tutorial.
|
||||
\newblock \emph{Rapport Technique}, 178, 1997.
|
||||
|
||||
\bibitem[K{\"a}stner et~al.(2017)K{\"a}stner, Leroy, Blazy, Schommer, Schmidt,
|
||||
and Ferdinand]{Kastner-et-al-2017}
|
||||
Daniel K{\"a}stner, Xavier Leroy, Sandrine Blazy, Bernhard Schommer, Michael
|
||||
Schmidt, and Christian Ferdinand.
|
||||
\newblock Closing the gap--the formally verified optimizing compiler compcert.
|
||||
\newblock In \emph{SSS'17: Safety-critical Systems Symposium 2017}, pages
|
||||
163--180. CreateSpace, 2017.
|
||||
|
||||
\bibitem[Kiselyov(2009)]{Kiselyov-2009}
|
||||
Oleg Kiselyov.
|
||||
\newblock Formalizing languages, mechanizing type-soundess and other
|
||||
meta-theoretic proofs, 2009.
|
||||
\newblock URL \url{http://okmij.org/ftp/formalizations/index.html}.
|
||||
|
||||
\bibitem[Klein et~al.(2009)Klein, Elphinstone, Heiser, Andronick, Cock, Derrin,
|
||||
Elkaduwe, Engelhardt, Kolanski, Norrish, et~al.]{Klein-2009}
|
||||
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock,
|
||||
Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael
|
||||
Norrish, et~al.
|
||||
\newblock sel4: Formal verification of an os kernel.
|
||||
\newblock In \emph{Proceedings of the ACM SIGOPS 22nd symposium on Operating
|
||||
systems principles}, pages 207--220. ACM, 2009.
|
||||
|
||||
\bibitem[Leroy(2009)]{Leroy-2009}
|
||||
Xavier Leroy.
|
||||
\newblock Formal verification of a realistic compiler.
|
||||
\newblock \emph{Communications of the ACM}, 52\penalty0 (7):\penalty0 107--115,
|
||||
2009.
|
||||
|
||||
\bibitem[McBride(2005)]{McBride-2005}
|
||||
Conor McBride.
|
||||
\newblock Type-preserving renaming and substitution, 2005.
|
||||
\newblock unpublished manuscript.
|
||||
|
||||
\bibitem[McBride(2015)]{McBride-2015}
|
||||
Conor McBride.
|
||||
\newblock Turing-completeness totally free.
|
||||
\newblock In \emph{International Conference on Mathematics of Program
|
||||
Construction}, pages 257--275. Springer, 2015.
|
||||
|
||||
\bibitem[O'Connor et~al.(2016)O'Connor, Chen, Rizkallah, Amani, Lim, Murray,
|
||||
Nagashima, Sewell, and Klein]{O'Connor-2016}
|
||||
Liam O'Connor, Zilin Chen, Christine Rizkallah, Sidney Amani, Japheth Lim, Toby
|
||||
Murray, Yutaka Nagashima, Thomas Sewell, and Gerwin Klein.
|
||||
\newblock Refinement through restraint: Bringing down the cost of verification.
|
||||
\newblock In \emph{ICFP}, pages 89--102, 2016.
|
||||
|
||||
\bibitem[Pierce(2009)]{Pierce-2009}
|
||||
Benjamin~C Pierce.
|
||||
\newblock Lambda, {T}he {U}ltimate {TA}.
|
||||
\newblock In \emph{ICFP}, pages 121--22, 2009.
|
||||
|
||||
\bibitem[Pierce and Benjamin(2002)]{Pierce-2002}
|
||||
Benjamin~C Pierce and C~Benjamin.
|
||||
\newblock \emph{Types and programming languages}.
|
||||
\newblock MIT press, 2002.
|
||||
|
||||
\bibitem[Pierce et~al.(2010)Pierce, Casinghino, Gaboardi, Greenberg,
|
||||
Hri{\c{t}}cu, Sj{\"o}berg, and Yorgey]{Pierce-et-al-2010}
|
||||
Benjamin~C Pierce, Chris Casinghino, Marco Gaboardi, Michael Greenberg,
|
||||
C{\u{a}}t{\u{a}}lin Hri{\c{t}}cu, Vilhelm Sj{\"o}berg, and Brent Yorgey.
|
||||
\newblock \emph{Software foundations}.
|
||||
\newblock 2010.
|
||||
\newblock URL
|
||||
\url{\url{http://www.cis.upenn.edu/bcpierce/sf/current/index.html}}.
|
||||
|
||||
\bibitem[Ro{\c s}u and {\c S}erb{\u a}nu{\c t}{\u
|
||||
a}(2010)]{Rosu-Serbanuta-2010}
|
||||
Grigore Ro{\c s}u and Traian~Florin {\c S}erb{\u a}nu{\c t}{\u a}.
|
||||
\newblock An overview of the {K} semantic framework.
|
||||
\newblock \emph{Journal of Logic and Algebraic Programming}, 79\penalty0
|
||||
(6):\penalty0 397--434, 2010.
|
||||
|
||||
\bibitem[Stump(2016)]{Stump-2016}
|
||||
Aaron Stump.
|
||||
\newblock \emph{Verified functional programming in Agda}.
|
||||
\newblock Morgan \& Claypool, 2016.
|
||||
|
||||
\bibitem[Wright and Felleisen(1994)]{Wright-and-Felleisen-1994}
|
||||
Andrew~K Wright and Matthias Felleisen.
|
||||
\newblock A syntactic approach to type soundness.
|
||||
\newblock \emph{Information and computation}, 115\penalty0 (1):\penalty0
|
||||
38--94, 1994.
|
||||
|
||||
\end{thebibliography}
|
||||
|
|
@ -1,52 +0,0 @@
|
|||
This is BibTeX, Version 0.99d (TeX Live 2016)
|
||||
Capacity: max_strings=35307, hash_size=35307, hash_prime=30011
|
||||
The top-level auxiliary file: PLFA.aux
|
||||
The style file: plainnat.bst
|
||||
Database file #1: PLFA.bib
|
||||
Warning--entry type for "Kiselyov-2009" isn't style-file defined
|
||||
--line 154 of file PLFA.bib
|
||||
Warning--entry type for "McBride-2005" isn't style-file defined
|
||||
--line 181 of file PLFA.bib
|
||||
Warning--empty publisher in Pierce-et-al-2010
|
||||
You've used 29 entries,
|
||||
2773 wiz_defined-function locations,
|
||||
773 strings with 10089 characters,
|
||||
and the built_in function-call counts, 15076 in all, are:
|
||||
= -- 1358
|
||||
> -- 881
|
||||
< -- 32
|
||||
+ -- 302
|
||||
- -- 273
|
||||
* -- 1109
|
||||
:= -- 2247
|
||||
add.period$ -- 100
|
||||
call.type$ -- 29
|
||||
change.case$ -- 170
|
||||
chr.to.int$ -- 29
|
||||
cite$ -- 59
|
||||
duplicate$ -- 727
|
||||
empty$ -- 1221
|
||||
format.name$ -- 316
|
||||
if$ -- 3269
|
||||
int.to.chr$ -- 1
|
||||
int.to.str$ -- 1
|
||||
missing$ -- 30
|
||||
newline$ -- 154
|
||||
num.names$ -- 116
|
||||
pop$ -- 413
|
||||
preamble$ -- 1
|
||||
purify$ -- 146
|
||||
quote$ -- 0
|
||||
skip$ -- 586
|
||||
stack$ -- 0
|
||||
substring$ -- 522
|
||||
swap$ -- 154
|
||||
text.length$ -- 14
|
||||
text.prefix$ -- 0
|
||||
top$ -- 0
|
||||
type$ -- 294
|
||||
warning$ -- 1
|
||||
while$ -- 132
|
||||
width$ -- 0
|
||||
write$ -- 389
|
||||
(There were 3 warnings)
|
||||
|
|
@ -1,133 +0,0 @@
|
|||
# Fdb version 3
|
||||
["bibtex PLFA"] 1532009241 "PLFA.aux" "PLFA.bbl" "PLFA" 1532009700
|
||||
"/usr/local/texlive/2016/texmf-dist/bibtex/bst/natbib/plainnat.bst" 1233624470 26816 ffe5423d2019860bad9f54bc402fac15 ""
|
||||
"PLFA.aux" 1532009700 6113 6614a450ede803c1dbcd58e21464b233 ""
|
||||
"PLFA.bcf" 0 -1 0 ""
|
||||
"PLFA.bib" 1532008100 8469 859d9ec6cd6d9f89accaa07f5c67b64f ""
|
||||
(generated)
|
||||
"PLFA.bbl"
|
||||
"PLFA.blg"
|
||||
["pdflatex"] 1532009698 "latex/PLFA.tex" "PLFA.pdf" "PLFA" 1532009700
|
||||
"/Users/wadler/Library/texmf/tex/latex/graphics.cfg" 1386002145 1599 cc574e5c201b0aea0b14dad7e51fd367 ""
|
||||
"/Users/wadler/Library/texmf/tex/latex/graphics.sty" 1386002145 14133 c544b57013763cf11c5032a5edfe9eb9 ""
|
||||
"/Users/wadler/Library/texmf/tex/latex/graphicx.sty" 1386002145 7882 3bd78469d444e8d494e27cfd7ca92719 ""
|
||||
"/Users/wadler/Library/texmf/tex/latex/keyval.sty" 1386002145 2266 7054435e4584a41cf53b0a7ca624d0cb ""
|
||||
"/Users/wadler/Library/texmf/tex/latex/pdftex.def" 1386002145 30724 58dbba8517ed26c9a85e9b6276394761 ""
|
||||
"/Users/wadler/Library/texmf/tex/latex/size10.clo" 1386002145 9027 74b699c9c45c28e76d49d24597aa1d0c ""
|
||||
"/Users/wadler/Library/texmf/tex/latex/supp-pdf.tex" 1386002145 75993 121f890a0f3bd94be4aac619bd0814ff ""
|
||||
"/Users/wadler/Library/texmf/tex/latex/trig.sty" 1386002145 3153 c50e6bd54d2dd3933fc52bcf369bec4a ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/enc/dvips/cm-super/cm-super-t1.enc" 1136849721 2971 def0b6c1f0b107b3b936def894055589 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/enc/dvips/stix/stix-t1.enc" 1388795362 7013 c55cc8669071ac14036c4a0c96c16202 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/enc/dvips/stix/stix-ts1.enc" 1388795362 2836 154e6b0061f9b8cb549144b55b268339 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/map/fontname/texfonts.map" 1272929888 3287 e6b82fe08f5336d4d5ebc73fb1152e87 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/jknappen/ec/ecbx1000.tfm" 1136768653 3584 2d666ecf6d466d8b007246bc2f94d9da ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/jknappen/ec/ecrm1000.tfm" 1136768653 3584 adb004a0c8e7c46ee66cad73671f37b4 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/jknappen/ec/ecsl1000.tfm" 1136768653 3584 bf02fd9e8bc8c375f218c700cabb9a92 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/jknappen/ec/ecss1000.tfm" 1136768653 3584 ab55608ad377891510479d34d90acc46 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/jknappen/ec/ecti1000.tfm" 1136768653 3072 3bce340d4c075dffe6d4ec732b4c32fe ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/jknappen/ec/ectt0900.tfm" 1136768653 1536 ae7aab2f8a4bc9edfce2899f53ba88c3 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/jknappen/ec/ectt1000.tfm" 1136768653 1536 06717a2b50de47d4087ac0e6cd759455 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm" 1246382020 916 f87d7c45f9c908e672703b83b72241a3 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam5.tfm" 1246382020 924 9904cf1d39e9767e7a3622f2a125a565 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam7.tfm" 1246382020 928 2dc8d444221b7a635bb58038579b861a ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm" 1246382020 908 2921f8a10601f252058503cc6570e581 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm5.tfm" 1246382020 940 75ac932a52f80982a9f8ea75d03a34cf ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm7.tfm" 1246382020 940 228d6584342e91276bf566bcf9716b83 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathbb.tfm" 1388795362 1628 082e94509983dd1f77a7fdc44f712932 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathbbit.tfm" 1388795362 2168 30d194a5875ada3505ad6a8c1bb54dea ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathcal.tfm" 1388795362 2220 4be0194a42d141b33fa339861ecefc51 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathex.tfm" 1388795362 1688 489fb532c51deab26c3df298066f58df ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathfrak.tfm" 1388795362 1768 da596289b8f971781ec2fb6de90ff57a ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathit.tfm" 1388795362 2596 a4f4d4c3140489d19337632bb9606bfc ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathrm-bold.tfm" 1388795362 2352 51bd9695f0569e4c1bde610dbf15aab0 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathrm.tfm" 1388795362 4204 1d0ae738a61b3caef3827dded5be7ce9 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathscr.tfm" 1388795362 2216 878c5adb7b08e5e5fd53a46a118e846b ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathsf.tfm" 1388795362 2084 2f1e8b09f7f218e2a7053ef95384ebe1 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathsfit.tfm" 1388795362 2560 304766c612fce5d4ce94849df0676616 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathtt.tfm" 1388795362 1396 56f228418b8da227ec737e2e8eb165ee ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/t1-stixgeneral-bold.tfm" 1388795362 11012 fe8465b2dc4812fb0ce069fcb0fe6af8 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/t1-stixgeneral-italic.tfm" 1388795362 11156 e8d76832153748248385d623691129d7 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/t1-stixgeneral.tfm" 1388795362 11184 42ce9dfc058df87da7094b2e2fab1260 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/ts1-stixgeneral.tfm" 1388795362 1420 a3fb73e1fffd188e53dd5a0b1edb271e ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/type1/public/cm-super/sftt0900.pfb" 1215737283 170827 2e4b634de7b58578eae1dc93e51dfe48 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/type1/public/cm-super/sftt1000.pfb" 1215737283 169201 9ebf99020dde51a5086e186761a34e8f ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/STIXGeneral-Bold.pfb" 1388795362 250376 86937501504e07e9745bc88e006094b2 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/STIXGeneral-Italic.pfb" 1388795362 221139 7b7742dd20e0010cb85b7f92956bac16 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/STIXGeneral-Regular.pfb" 1388795362 547522 a9135ac84940b576091fbefc78a79500 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/stix-mathfrak.pfb" 1388795362 46278 ca6764f9454c2124ef03fc6659dc6d02 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/stix-mathit.pfb" 1388795362 41474 772656494141d29334d3e80c9a859c10 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/stix-mathrm.pfb" 1388795362 40662 35fc2ef7e5426524c472184c87cb4d57 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/stix-mathsf.pfb" 1388795362 41655 e7591451a427b4270d35622721b08f6a ""
|
||||
"/usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/stix-mathtt.pfb" 1388795362 33345 eed8935644a2e407434be96adf5ada36 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/generic/ifxetex/ifxetex.sty" 1284331290 1458 43ab4710dc82f3edeabecd0d099626b2 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/ifluatex.sty" 1463608860 7324 2310d1247db0114eb4726807c8837a0e ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/amsfonts.sty" 1359763108 5949 3f3fd50a8cc94c3d4cbf4fc66cd3df1c ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/amssymb.sty" 1359763108 13829 94730e64147574077f8ecfea9bb69af4 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/umsa.fd" 1359763108 961 6518c6525a34feb5e8250ffa91731cff ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/umsb.fd" 1359763108 961 d02606146ba5601b5645f987c92e6193 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/base/article.cls" 1459635588 19821 310da678527a7dfe2a02c88af38079b7 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/base/fontenc.sty" 1454284088 4572 634fcdf7e9df867d6d54f84638930408 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/base/ifthen.sty" 1454284088 5159 a08c9bbd48fc492f15b22e458bef961f ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/base/inputenc.sty" 1459635588 4732 d63eda807ac82cca2ca8488efd31a966 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/base/t1cmss.fd" 1454284088 2408 9332529df2b0aa93e638793f315828fc ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/base/t1cmtt.fd" 1454284088 2230 5ebc5467205143c6f21bcc41d27910c1 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/base/t1enc.def" 1454284088 9927 925418b4e40d02671b4728df100ec5ef ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/base/textcomp.sty" 1454284088 16155 3b0b2cc7c05e0ccf8c3ce5da21d4bccb ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/base/ts1cmr.fd" 1454284088 2217 d274654bda1292013bdf48d5f720a495 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/base/ts1enc.def" 1454284088 7767 aa88823823f5e767d79ea1166ab1ae74 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/carlisle/remreset.sty" 1137109962 1096 6a75275ca00e32428c6f059d2f618ea7 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/environ/environ.sty" 1399239813 4378 f429f0da968c278653359293040a8f52 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/etoolbox/etoolbox.sty" 1438639395 41547 7860e623236f5f726a4099bbb7dd89fb ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/graphics-cfg/color.cfg" 1459978653 1213 620bba36b25224fa9b7e1ccb4ecb76fd ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/ifmtarg/ifmtarg.sty" 1278810218 438 4c0f57b7cba6e6ca9226b32da26f82e9 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/lazylist/lazylist.sty" 1137110265 2645 d3f23b6a73334ab7769a4322eb1e4557 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/natbib/natbib.sty" 1291685959 45456 1c8843383c0bd05870c45fa0ebea6cc2 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/oberdiek/aliascnt.sty" 1463608860 2511 9250ac9a7cafca5bf9264add9b635239 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/polytable/polytable.sty" 1374190213 26448 97a33bcf6337bfdc224deccebb3dde3c ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stix.fd" 1429396547 1801 77f24a4de2d640f19d644cf489bab946 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stixbb.fd" 1429396547 1773 e9ba3b0984306a374d47149e34079f58 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stixfrak.fd" 1429396547 1665 c8d9f4701ba9c1de147e39bd5ba24690 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stixscr.fd" 1429396547 1720 56c1328644c6db963a09482ae3d1330b ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stixsf.fd" 1429396547 1838 38b802cf506b108ef75e1fd5872a8133 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls2stix.fd" 1429396547 1801 bf9e70e07e7ec0abfc983dabb9a955ad ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls2stixcal.fd" 1429396547 1661 2167878d1897d8d5bd29ccaa76ee19b4 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls2stixex.fd" 1429396547 1632 76008671c8e2e1a12281fb78d3e34f15 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls2stixtt.fd" 1429396547 1650 17f864699a46f12cf4c2bb97bd4c7768 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/stix/stix.sty" 1429396547 127748 3600f2b18eec391b69a22a7212d38492 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/stix/t1stix.fd" 1429396547 2214 8c074e05c4ef5af520f739918e222af4 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ts1stix.fd" 1429396547 2227 3023591354ba6ccf3a61923e27246aae ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/tipa/t3cmr.fd" 1137110956 1257 fd5b1c2f0106f9cf12cdb2ff961987c5 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/tipa/t3enc.def" 1137110956 26483 c461a68c34040cb0d96c43e86c012a6d ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/tipa/tipa.sty" 1137110956 21394 82fa9965637ca62399434739ae5998f6 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/tools/array.sty" 1459635588 12398 bd782945c489f84ff012bcea4a712d25 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/tools/calc.sty" 1454284088 10214 d03d065f799d54f6b7e9b175f8d84279 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/tools/multicol.sty" 1462659744 29824 08f95a42addbc2524015cbf3bc7ad24a ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/trimspaces/trimspaces.sty" 1253232110 1380 971a51b00a14503ddf754cab24c3f209 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/data/uni-32.def" 1368571634 8033 ee5a06eead35a732222f876800c8f10f ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/data/uni-33.def" 1368571634 8589 ed28b1c7dfc407d19d76bca04a0a8153 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/data/uni-global.def" 1368571634 1375 8a855db83af5d6753ccbbd32e6a8a901 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/ucs.sty" 1368571634 27982 5723d81d568db410592a59b85fb3eaae ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/ucsencs.def" 1368571634 22368 c53c9d0d16c65bef2b157515c9d9f658 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/utf8x.def" 1368571634 8036 21f7ac37aafb6cfeddbb196b8bfd6280 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/url/url.sty" 1388531844 12796 8edb7d69a20b857904dd0ea757c14ec9 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/xcolor/xcolor.sty" 1463002160 55589 34128738f682d033422ca125f82e5d62 ""
|
||||
"/usr/local/texlive/2016/texmf-dist/tex/latex/xifthen/xifthen.sty" 1448319911 5689 1bfa68243e89a54479e7d0580773c57e ""
|
||||
"/usr/local/texlive/2016/texmf-dist/web2c/texmf.cnf" 1463093894 31953 b9489e6e586f798610c60aec1f5ec548 ""
|
||||
"/usr/local/texlive/2016/texmf-var/fonts/map/pdftex/updmap/pdftex.map" 1486125564 1888048 f2c5faed5981a516f406b2ccc20bff71 ""
|
||||
"/usr/local/texlive/2016/texmf-var/web2c/pdftex/pdflatex.fmt" 1486125600 3873396 effdf697f72257bb1888c504cc0bfe5a ""
|
||||
"/usr/local/texlive/2016/texmf.cnf" 1463979140 577 2938757e76f31531e65cc647e3507693 ""
|
||||
"PLFA.aux" 1532009700 6113 6614a450ede803c1dbcd58e21464b233 ""
|
||||
"PLFA.bbl" 1532009241 8064 873f028b7d884f51642fd5e1d62632c8 "bibtex PLFA"
|
||||
"agda.sty" 1531086217 23792 d8a4bc8eeae2f369807d7ee7bd1ca6b8 ""
|
||||
"figures/plfa-eval.png" 1531145889 245491 e66619f21eb55db25d35a2ae715266b2 ""
|
||||
"figures/plfa-progress-1.png" 1530898363 281201 995f81735adc44645f97b9d325258540 ""
|
||||
"figures/plfa-progress-2.png" 1530898520 216038 81541c95a5ac859110cdb380ff67127d ""
|
||||
"figures/plfa-progress-3a.png" 1530987887 368107 bb17da40310533d6a58bf365dbfda912 ""
|
||||
"figures/sf-progress-1.png" 1530898077 387655 a1ef617726db0ef8c8c807b4fdc696ea ""
|
||||
"figures/sf-progress-2.png" 1530898202 265849 5148ca2b1544d1c04d753dea7a380739 ""
|
||||
"latex/PLFA.tex" 1532009698 32248 e9f41b27c953abadf7c7c0b35d1462db ""
|
||||
"llncs.cls" 1530716752 43467 a21466011e5ed5d4c3f1d5a9af897395 ""
|
||||
(generated)
|
||||
"PLFA.aux"
|
||||
"PLFA.log"
|
||||
"PLFA.pdf"
|
||||
258
sbmf/PLFA.fls
258
sbmf/PLFA.fls
|
|
@ -1,258 +0,0 @@
|
|||
PWD /Users/wadler/wadler/papers/sbmf
|
||||
INPUT /usr/local/texlive/2016/texmf.cnf
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/web2c/texmf.cnf
|
||||
INPUT /usr/local/texlive/2016/texmf-var/web2c/pdftex/pdflatex.fmt
|
||||
INPUT latex/PLFA.tex
|
||||
OUTPUT PLFA.log
|
||||
INPUT llncs.cls
|
||||
INPUT llncs.cls
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/article.cls
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/article.cls
|
||||
INPUT /Users/wadler/Library/texmf/tex/latex/size10.clo
|
||||
INPUT /Users/wadler/Library/texmf/tex/latex/size10.clo
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/tools/multicol.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/tools/multicol.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/oberdiek/aliascnt.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/oberdiek/aliascnt.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/carlisle/remreset.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/carlisle/remreset.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/natbib/natbib.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/natbib/natbib.sty
|
||||
INPUT agda.sty
|
||||
INPUT agda.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/generic/ifxetex/ifxetex.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/generic/ifxetex/ifxetex.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/ifluatex.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/ifluatex.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/xifthen/xifthen.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/xifthen/xifthen.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/tools/calc.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/tools/calc.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/ifthen.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/ifthen.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/ifmtarg/ifmtarg.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/ifmtarg/ifmtarg.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/xcolor/xcolor.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/xcolor/xcolor.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/graphics-cfg/color.cfg
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/graphics-cfg/color.cfg
|
||||
INPUT /Users/wadler/Library/texmf/tex/latex/pdftex.def
|
||||
INPUT /Users/wadler/Library/texmf/tex/latex/pdftex.def
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/polytable/polytable.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/polytable/polytable.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/lazylist/lazylist.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/lazylist/lazylist.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/tools/array.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/tools/array.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/etoolbox/etoolbox.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/etoolbox/etoolbox.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/environ/environ.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/environ/environ.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/trimspaces/trimspaces.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/trimspaces/trimspaces.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/ucs/ucs.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/ucs/ucs.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/ucs/data/uni-global.def
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/ucs/data/uni-global.def
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/inputenc.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/inputenc.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/ucs/utf8x.def
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/ucs/utf8x.def
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/fontenc.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/fontenc.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/t1enc.def
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/t1enc.def
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/map/fontname/texfonts.map
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/jknappen/ec/ecrm1000.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/amsfonts.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/amsfonts.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/amssymb.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/amssymb.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/tipa/tipa.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/tipa/tipa.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/fontenc.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/fontenc.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/tipa/t3enc.def
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/tipa/t3enc.def
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/jknappen/ec/ecsl1000.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/jknappen/ec/ecti1000.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/jknappen/ec/ecbx1000.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/t1cmss.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/t1cmss.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/jknappen/ec/ecss1000.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/t1enc.def
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/t1enc.def
|
||||
INPUT /Users/wadler/Library/texmf/tex/latex/graphicx.sty
|
||||
INPUT /Users/wadler/Library/texmf/tex/latex/graphicx.sty
|
||||
INPUT /Users/wadler/Library/texmf/tex/latex/keyval.sty
|
||||
INPUT /Users/wadler/Library/texmf/tex/latex/keyval.sty
|
||||
INPUT /Users/wadler/Library/texmf/tex/latex/graphics.sty
|
||||
INPUT /Users/wadler/Library/texmf/tex/latex/graphics.sty
|
||||
INPUT /Users/wadler/Library/texmf/tex/latex/trig.sty
|
||||
INPUT /Users/wadler/Library/texmf/tex/latex/trig.sty
|
||||
INPUT /Users/wadler/Library/texmf/tex/latex/graphics.cfg
|
||||
INPUT /Users/wadler/Library/texmf/tex/latex/graphics.cfg
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/url/url.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/url/url.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/stix.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/stix.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/textcomp.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/textcomp.sty
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/ts1enc.def
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/ts1enc.def
|
||||
INPUT PLFA.aux
|
||||
INPUT PLFA.aux
|
||||
OUTPUT PLFA.aux
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/tipa/t3cmr.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/tipa/t3cmr.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/ts1cmr.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/ts1cmr.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stix.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stix.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls2stix.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls2stix.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/t1stix.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/t1stix.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/t1-stixgeneral.tfm
|
||||
INPUT /Users/wadler/Library/texmf/tex/latex/supp-pdf.tex
|
||||
INPUT /Users/wadler/Library/texmf/tex/latex/supp-pdf.tex
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/ucs/ucsencs.def
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/ucs/ucsencs.def
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/t1-stixgeneral.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/t1-stixgeneral-bold.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathrm.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathrm.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathrm.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathit.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathit.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathit.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stixscr.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stixscr.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathscr.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathscr.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathscr.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls2stixex.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls2stixex.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathex.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathex.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathex.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/umsa.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/umsa.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam7.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam7.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/umsb.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/umsb.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm7.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm7.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathrm-bold.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathrm-bold.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathrm-bold.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stixfrak.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stixfrak.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathfrak.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathfrak.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathfrak.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stixbb.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stixbb.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathbb.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathbb.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathbb.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathbbit.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathbbit.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathbbit.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls2stixcal.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls2stixcal.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathcal.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathcal.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathcal.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stixsf.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stixsf.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathsf.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathsf.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathsf.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathsfit.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathsfit.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathsfit.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls2stixtt.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls2stixtt.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathtt.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathtt.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathtt.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/t1-stixgeneral.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/t1cmtt.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/base/t1cmtt.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/jknappen/ec/ectt0900.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/t1-stixgeneral-bold.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/t1-stixgeneral-italic.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathrm.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathrm.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathit.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathit.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathscr.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathscr.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathex.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathex.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam10.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/amsfonts/symbols/msam5.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm10.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/amsfonts/symbols/msbm5.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathrm-bold.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathrm-bold.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathfrak.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathfrak.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathbb.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathbb.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathbbit.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathbbit.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathcal.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathcal.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathsf.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathsf.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathsfit.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathsfit.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathtt.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/stix-mathtt.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ts1stix.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/stix/ts1stix.fd
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/ts1-stixgeneral.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/t1-stixgeneral.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/t1-stixgeneral-bold.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/t1-stixgeneral-italic.tfm
|
||||
OUTPUT PLFA.pdf
|
||||
INPUT /usr/local/texlive/2016/texmf-var/fonts/map/pdftex/updmap/pdftex.map
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/jknappen/ec/ectt1000.tfm
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/stix/t1-stixgeneral-bold.tfm
|
||||
INPUT figures/plfa-progress-1.png
|
||||
INPUT ./figures/plfa-progress-1.png
|
||||
INPUT figures/plfa-progress-2.png
|
||||
INPUT ./figures/plfa-progress-2.png
|
||||
INPUT figures/plfa-progress-3a.png
|
||||
INPUT ./figures/plfa-progress-3a.png
|
||||
INPUT figures/sf-progress-1.png
|
||||
INPUT ./figures/sf-progress-1.png
|
||||
INPUT figures/sf-progress-2.png
|
||||
INPUT ./figures/sf-progress-2.png
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/ucs/data/uni-32.def
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/ucs/data/uni-32.def
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/ucs/data/uni-33.def
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/ucs/data/uni-33.def
|
||||
INPUT figures/plfa-eval.png
|
||||
INPUT ./figures/plfa-eval.png
|
||||
INPUT PLFA.bbl
|
||||
INPUT PLFA.bbl
|
||||
INPUT PLFA.aux
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/enc/dvips/cm-super/cm-super-t1.enc
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/enc/dvips/stix/stix-ts1.enc
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/enc/dvips/stix/stix-t1.enc
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/STIXGeneral-Bold.pfb
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/STIXGeneral-Italic.pfb
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/STIXGeneral-Regular.pfb
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/type1/public/cm-super/sftt0900.pfb
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/type1/public/cm-super/sftt1000.pfb
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/stix-mathfrak.pfb
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/stix-mathit.pfb
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/stix-mathrm.pfb
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/stix-mathsf.pfb
|
||||
INPUT /usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/stix-mathtt.pfb
|
||||
707
sbmf/PLFA.log
707
sbmf/PLFA.log
|
|
@ -1,707 +0,0 @@
|
|||
This is pdfTeX, Version 3.14159265-2.6-1.40.17 (TeX Live 2016) (preloaded format=pdflatex 2017.2.3) 19 JUL 2018 16:14
|
||||
entering extended mode
|
||||
restricted \write18 enabled.
|
||||
%&-line parsing enabled.
|
||||
**latex/PLFA.tex
|
||||
(./latex/PLFA.tex
|
||||
LaTeX2e <2016/03/31>
|
||||
Babel <3.9r> and hyphenation patterns for 83 language(s) loaded.
|
||||
(./llncs.cls
|
||||
Document Class: llncs 2018/03/10 v2.20
|
||||
LaTeX document class for Lecture Notes in Computer Science
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/article.cls
|
||||
Document Class: article 2014/09/29 v1.4h Standard LaTeX document class
|
||||
(/Users/wadler/Library/texmf/tex/latex/size10.clo
|
||||
File: size10.clo 2005/09/16 v1.4f Standard LaTeX file (size option)
|
||||
)
|
||||
\c@part=\count79
|
||||
\c@section=\count80
|
||||
\c@subsection=\count81
|
||||
\c@subsubsection=\count82
|
||||
\c@paragraph=\count83
|
||||
\c@subparagraph=\count84
|
||||
\c@figure=\count85
|
||||
\c@table=\count86
|
||||
\abovecaptionskip=\skip41
|
||||
\belowcaptionskip=\skip42
|
||||
\bibindent=\dimen102
|
||||
)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/tools/multicol.sty
|
||||
Package: multicol 2016/04/07 v1.8p multicolumn formatting (FMi)
|
||||
\c@tracingmulticols=\count87
|
||||
\mult@box=\box26
|
||||
\multicol@leftmargin=\dimen103
|
||||
\c@unbalance=\count88
|
||||
\c@collectmore=\count89
|
||||
\doublecol@number=\count90
|
||||
\multicoltolerance=\count91
|
||||
\multicolpretolerance=\count92
|
||||
\full@width=\dimen104
|
||||
\page@free=\dimen105
|
||||
\premulticols=\dimen106
|
||||
\postmulticols=\dimen107
|
||||
\multicolsep=\skip43
|
||||
\multicolbaselineskip=\skip44
|
||||
\partial@page=\box27
|
||||
\last@line=\box28
|
||||
\maxbalancingoverflow=\dimen108
|
||||
\mult@rightbox=\box29
|
||||
\mult@grightbox=\box30
|
||||
\mult@gfirstbox=\box31
|
||||
\mult@firstbox=\box32
|
||||
\@tempa=\box33
|
||||
\@tempa=\box34
|
||||
\@tempa=\box35
|
||||
\@tempa=\box36
|
||||
\@tempa=\box37
|
||||
\@tempa=\box38
|
||||
\@tempa=\box39
|
||||
\@tempa=\box40
|
||||
\@tempa=\box41
|
||||
\@tempa=\box42
|
||||
\@tempa=\box43
|
||||
\@tempa=\box44
|
||||
\@tempa=\box45
|
||||
\@tempa=\box46
|
||||
\@tempa=\box47
|
||||
\@tempa=\box48
|
||||
\@tempa=\box49
|
||||
\c@columnbadness=\count93
|
||||
\c@finalcolumnbadness=\count94
|
||||
\last@try=\dimen109
|
||||
\multicolovershoot=\dimen110
|
||||
\multicolundershoot=\dimen111
|
||||
\mult@nat@firstbox=\box50
|
||||
\colbreak@box=\box51
|
||||
\mc@col@check@num=\count95
|
||||
)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/oberdiek/aliascnt.sty
|
||||
Package: aliascnt 2016/05/16 v1.4 Alias counters (HO)
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/carlisle/remreset.sty))
|
||||
\c@chapter=\count96
|
||||
LaTeX Font Info: Redeclaring math symbol \Gamma on input line 362.
|
||||
LaTeX Font Info: Redeclaring math symbol \Delta on input line 363.
|
||||
LaTeX Font Info: Redeclaring math symbol \Theta on input line 364.
|
||||
LaTeX Font Info: Redeclaring math symbol \Lambda on input line 365.
|
||||
LaTeX Font Info: Redeclaring math symbol \Xi on input line 366.
|
||||
LaTeX Font Info: Redeclaring math symbol \Pi on input line 367.
|
||||
LaTeX Font Info: Redeclaring math symbol \Sigma on input line 368.
|
||||
LaTeX Font Info: Redeclaring math symbol \Upsilon on input line 369.
|
||||
LaTeX Font Info: Redeclaring math symbol \Phi on input line 370.
|
||||
LaTeX Font Info: Redeclaring math symbol \Psi on input line 371.
|
||||
LaTeX Font Info: Redeclaring math symbol \Omega on input line 372.
|
||||
\tocchpnum=\dimen112
|
||||
\tocsecnum=\dimen113
|
||||
\tocsectotal=\dimen114
|
||||
\tocsubsecnum=\dimen115
|
||||
\tocsubsectotal=\dimen116
|
||||
\tocsubsubsecnum=\dimen117
|
||||
\tocsubsubsectotal=\dimen118
|
||||
\tocparanum=\dimen119
|
||||
\tocparatotal=\dimen120
|
||||
\tocsubparanum=\dimen121
|
||||
\@tempcntc=\count97
|
||||
\fnindent=\dimen122
|
||||
\c@@inst=\count98
|
||||
\c@@auth=\count99
|
||||
\c@auco=\count100
|
||||
\instindent=\dimen123
|
||||
\authrun=\box52
|
||||
\authorrunning=\toks14
|
||||
\tocauthor=\toks15
|
||||
\titrun=\box53
|
||||
\titlerunning=\toks16
|
||||
\toctitle=\toks17
|
||||
\c@theorem=\count101
|
||||
\c@case=\count102
|
||||
\c@conjecture=\count103
|
||||
\c@corollary=\count104
|
||||
\c@definition=\count105
|
||||
\c@example=\count106
|
||||
\c@exercise=\count107
|
||||
\c@lemma=\count108
|
||||
\c@note=\count109
|
||||
\c@problem=\count110
|
||||
\c@property=\count111
|
||||
\c@proposition=\count112
|
||||
\c@question=\count113
|
||||
\c@solution=\count114
|
||||
\c@remark=\count115
|
||||
\headlineindent=\dimen124
|
||||
)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/natbib/natbib.sty
|
||||
Package: natbib 2010/09/13 8.31b (PWD, AO)
|
||||
\bibhang=\skip45
|
||||
\bibsep=\skip46
|
||||
LaTeX Info: Redefining \cite on input line 694.
|
||||
\c@NAT@ctr=\count116
|
||||
) (./agda.sty
|
||||
Package: agda
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/generic/ifxetex/ifxetex.sty
|
||||
Package: ifxetex 2010/09/12 v0.6 Provides ifxetex conditional
|
||||
)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/ifluatex.sty
|
||||
Package: ifluatex 2016/05/16 v1.4 Provides the ifluatex switch (HO)
|
||||
Package ifluatex Info: LuaTeX not detected.
|
||||
)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/xifthen/xifthen.sty
|
||||
Package: xifthen 2015/11/05 v1.4.0 Extended ifthen features
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/tools/calc.sty
|
||||
Package: calc 2014/10/28 v4.3 Infix arithmetic (KKT,FJ)
|
||||
\calc@Acount=\count117
|
||||
\calc@Bcount=\count118
|
||||
\calc@Adimen=\dimen125
|
||||
\calc@Bdimen=\dimen126
|
||||
\calc@Askip=\skip47
|
||||
\calc@Bskip=\skip48
|
||||
LaTeX Info: Redefining \setlength on input line 80.
|
||||
LaTeX Info: Redefining \addtolength on input line 81.
|
||||
\calc@Ccount=\count119
|
||||
\calc@Cskip=\skip49
|
||||
)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/ifthen.sty
|
||||
Package: ifthen 2014/09/29 v1.1c Standard LaTeX ifthen package (DPC)
|
||||
)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/ifmtarg/ifmtarg.sty
|
||||
Package: ifmtarg 2009/09/02 v1.2a check for an empty argument
|
||||
))
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/xcolor/xcolor.sty
|
||||
Package: xcolor 2016/05/11 v2.12 LaTeX color extensions (UK)
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics-cfg/color.cfg
|
||||
File: color.cfg 2016/01/02 v1.6 sample color configuration
|
||||
)
|
||||
Package xcolor Info: Driver file: pdftex.def on input line 225.
|
||||
|
||||
(/Users/wadler/Library/texmf/tex/latex/pdftex.def
|
||||
File: pdftex.def 2007/01/08 v0.04d Graphics/color for pdfTeX
|
||||
\Gread@gobject=\count120
|
||||
)
|
||||
Package xcolor Info: Model `cmy' substituted by `cmy0' on input line 1348.
|
||||
Package xcolor Info: Model `hsb' substituted by `rgb' on input line 1352.
|
||||
Package xcolor Info: Model `RGB' extended on input line 1364.
|
||||
Package xcolor Info: Model `HTML' substituted by `rgb' on input line 1366.
|
||||
Package xcolor Info: Model `Hsb' substituted by `hsb' on input line 1367.
|
||||
Package xcolor Info: Model `tHsb' substituted by `hsb' on input line 1368.
|
||||
Package xcolor Info: Model `HSB' substituted by `hsb' on input line 1369.
|
||||
Package xcolor Info: Model `Gray' substituted by `gray' on input line 1370.
|
||||
Package xcolor Info: Model `wave' substituted by `hsb' on input line 1371.
|
||||
)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/polytable/polytable.sty
|
||||
Package: polytable 2013/07/18 v0.8.5 `polytable' package (Andres Loeh)
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/lazylist/lazylist.sty)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/tools/array.sty
|
||||
Package: array 2014/10/28 v2.4c Tabular extension package (FMi)
|
||||
\col@sep=\dimen127
|
||||
\extrarowheight=\dimen128
|
||||
\NC@list=\toks18
|
||||
\extratabsurround=\skip50
|
||||
\backup@length=\skip51
|
||||
)
|
||||
\PT@colwidth=\dimen129
|
||||
\PT@cols=\count121
|
||||
\PT@table=\count122
|
||||
\PT@toks=\toks19
|
||||
\PT@in=\read1
|
||||
\PT@out=\write3
|
||||
)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/etoolbox/etoolbox.sty
|
||||
Package: etoolbox 2015/08/02 v2.2a e-TeX tools for LaTeX (JAW)
|
||||
\etb@tempcnta=\count123
|
||||
)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/environ/environ.sty
|
||||
Package: environ 2014/05/04 v0.3 A new way to define environments
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/trimspaces/trimspaces.sty
|
||||
Package: trimspaces 2009/09/17 v1.1 Trim spaces around a token list
|
||||
)
|
||||
\@envbody=\toks20
|
||||
)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/ucs.sty
|
||||
Package: ucs 2013/05/11 v2.2 UCS: Unicode input support
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/data/uni-global.def
|
||||
File: uni-global.def 2013/05/13 UCS: Unicode global data
|
||||
)
|
||||
\uc@secondtry=\count124
|
||||
\uc@combtoks=\toks21
|
||||
\uc@combtoksb=\toks22
|
||||
\uc@temptokena=\toks23
|
||||
)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/inputenc.sty
|
||||
Package: inputenc 2015/03/17 v1.2c Input encoding file
|
||||
\inpenc@prehook=\toks24
|
||||
\inpenc@posthook=\toks25
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/utf8x.def
|
||||
File: utf8x.def 2004/10/17 UCS: Input encoding UTF-8
|
||||
))
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/fontenc.sty
|
||||
Package: fontenc 2005/09/27 v1.99g Standard LaTeX package
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/t1enc.def
|
||||
File: t1enc.def 2005/09/27 v1.99g Standard LaTeX file
|
||||
LaTeX Font Info: Redeclaring font encoding T1 on input line 48.
|
||||
))
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/amsfonts.sty
|
||||
Package: amsfonts 2013/01/14 v3.01 Basic AMSFonts support
|
||||
\@emptytoks=\toks26
|
||||
\symAMSa=\mathgroup4
|
||||
\symAMSb=\mathgroup5
|
||||
LaTeX Font Info: Overwriting math alphabet `\mathfrak' in version `bold'
|
||||
(Font) U/euf/m/n --> U/euf/b/n on input line 106.
|
||||
)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/amssymb.sty
|
||||
Package: amssymb 2013/01/14 v3.01 AMS font symbols
|
||||
)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/tipa/tipa.sty
|
||||
Package: tipa 2002/08/08 TIPA version 1.1
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/fontenc.sty
|
||||
Package: fontenc 2005/09/27 v1.99g Standard LaTeX package
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/tipa/t3enc.def
|
||||
File: t3enc.def 2001/12/31 T3 encoding
|
||||
LaTeX Font Info: Try loading font information for T1+cmss on input line 357.
|
||||
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/t1cmss.fd
|
||||
File: t1cmss.fd 2014/09/29 v2.5h Standard LaTeX font definitions
|
||||
))
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/t1enc.def
|
||||
File: t1enc.def 2005/09/27 v1.99g Standard LaTeX file
|
||||
LaTeX Font Info: Redeclaring font encoding T1 on input line 48.
|
||||
)))
|
||||
\mathindent=\dimen130
|
||||
\c@Agda@Current=\count125
|
||||
\c@Agda@Previous=\count126
|
||||
\c@Agda@AlignStart=\count127
|
||||
\c@Agda@SuppressStart=\count128
|
||||
\AgdaEmptySkip=\skip52
|
||||
\AgdaEmptyExtraSkip=\skip53
|
||||
)
|
||||
(/Users/wadler/Library/texmf/tex/latex/graphicx.sty
|
||||
Package: graphicx 1999/02/16 v1.0f Enhanced LaTeX Graphics (DPC,SPQR)
|
||||
|
||||
(/Users/wadler/Library/texmf/tex/latex/keyval.sty
|
||||
Package: keyval 1999/03/16 v1.13 key=value parser (DPC)
|
||||
\KV@toks@=\toks27
|
||||
)
|
||||
(/Users/wadler/Library/texmf/tex/latex/graphics.sty
|
||||
Package: graphics 2006/02/20 v1.0o Standard LaTeX Graphics (DPC,SPQR)
|
||||
|
||||
(/Users/wadler/Library/texmf/tex/latex/trig.sty
|
||||
Package: trig 1999/03/16 v1.09 sin cos tan (DPC)
|
||||
)
|
||||
(/Users/wadler/Library/texmf/tex/latex/graphics.cfg
|
||||
File: graphics.cfg 2007/01/18 v1.5 graphics configuration of teTeX/TeXLive
|
||||
)
|
||||
Package graphics Info: Driver file: pdftex.def on input line 90.
|
||||
)
|
||||
\Gin@req@height=\dimen131
|
||||
\Gin@req@width=\dimen132
|
||||
)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/url/url.sty
|
||||
\Urlmuskip=\muskip10
|
||||
Package: url 2013/09/16 ver 3.4 Verb mode for urls, etc.
|
||||
)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/stix/stix.sty
|
||||
Package: stix 2015/04/17 v1.1.2-latex STIX fonts support package
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/textcomp.sty
|
||||
Package: textcomp 2005/09/27 v1.99g Standard LaTeX package
|
||||
Package textcomp Info: Sub-encoding information:
|
||||
(textcomp) 5 = only ISO-Adobe without \textcurrency
|
||||
(textcomp) 4 = 5 + \texteuro
|
||||
(textcomp) 3 = 4 + \textohm
|
||||
(textcomp) 2 = 3 + \textestimated + \textcurrency
|
||||
(textcomp) 1 = TS1 - \textcircled - \t
|
||||
(textcomp) 0 = TS1 (full)
|
||||
(textcomp) Font families with sub-encoding setting implement
|
||||
(textcomp) only a restricted character set as indicated.
|
||||
(textcomp) Family '?' is the default used for unknown fonts.
|
||||
(textcomp) See the documentation for details.
|
||||
Package textcomp Info: Setting ? sub-encoding to TS1/1 on input line 79.
|
||||
Package textcomp Info: Changing ? sub-encoding to TS1/0 on input line 80.
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/ts1enc.def
|
||||
File: ts1enc.def 2001/06/05 v3.0e (jk/car/fm) Standard LaTeX file
|
||||
)
|
||||
LaTeX Info: Redefining \oldstylenums on input line 334.
|
||||
Package textcomp Info: Setting cmr sub-encoding to TS1/0 on input line 349.
|
||||
Package textcomp Info: Setting cmss sub-encoding to TS1/0 on input line 350.
|
||||
Package textcomp Info: Setting cmtt sub-encoding to TS1/0 on input line 351.
|
||||
Package textcomp Info: Setting cmvtt sub-encoding to TS1/0 on input line 352.
|
||||
Package textcomp Info: Setting cmbr sub-encoding to TS1/0 on input line 353.
|
||||
Package textcomp Info: Setting cmtl sub-encoding to TS1/0 on input line 354.
|
||||
Package textcomp Info: Setting ccr sub-encoding to TS1/0 on input line 355.
|
||||
Package textcomp Info: Setting ptm sub-encoding to TS1/4 on input line 356.
|
||||
Package textcomp Info: Setting pcr sub-encoding to TS1/4 on input line 357.
|
||||
Package textcomp Info: Setting phv sub-encoding to TS1/4 on input line 358.
|
||||
Package textcomp Info: Setting ppl sub-encoding to TS1/3 on input line 359.
|
||||
Package textcomp Info: Setting pag sub-encoding to TS1/4 on input line 360.
|
||||
Package textcomp Info: Setting pbk sub-encoding to TS1/4 on input line 361.
|
||||
Package textcomp Info: Setting pnc sub-encoding to TS1/4 on input line 362.
|
||||
Package textcomp Info: Setting pzc sub-encoding to TS1/4 on input line 363.
|
||||
Package textcomp Info: Setting bch sub-encoding to TS1/4 on input line 364.
|
||||
Package textcomp Info: Setting put sub-encoding to TS1/5 on input line 365.
|
||||
Package textcomp Info: Setting uag sub-encoding to TS1/5 on input line 366.
|
||||
Package textcomp Info: Setting ugq sub-encoding to TS1/5 on input line 367.
|
||||
Package textcomp Info: Setting ul8 sub-encoding to TS1/4 on input line 368.
|
||||
Package textcomp Info: Setting ul9 sub-encoding to TS1/4 on input line 369.
|
||||
Package textcomp Info: Setting augie sub-encoding to TS1/5 on input line 370.
|
||||
Package textcomp Info: Setting dayrom sub-encoding to TS1/3 on input line 371.
|
||||
Package textcomp Info: Setting dayroms sub-encoding to TS1/3 on input line 372.
|
||||
|
||||
Package textcomp Info: Setting pxr sub-encoding to TS1/0 on input line 373.
|
||||
Package textcomp Info: Setting pxss sub-encoding to TS1/0 on input line 374.
|
||||
Package textcomp Info: Setting pxtt sub-encoding to TS1/0 on input line 375.
|
||||
Package textcomp Info: Setting txr sub-encoding to TS1/0 on input line 376.
|
||||
Package textcomp Info: Setting txss sub-encoding to TS1/0 on input line 377.
|
||||
Package textcomp Info: Setting txtt sub-encoding to TS1/0 on input line 378.
|
||||
Package textcomp Info: Setting lmr sub-encoding to TS1/0 on input line 379.
|
||||
Package textcomp Info: Setting lmdh sub-encoding to TS1/0 on input line 380.
|
||||
Package textcomp Info: Setting lmss sub-encoding to TS1/0 on input line 381.
|
||||
Package textcomp Info: Setting lmssq sub-encoding to TS1/0 on input line 382.
|
||||
Package textcomp Info: Setting lmvtt sub-encoding to TS1/0 on input line 383.
|
||||
Package textcomp Info: Setting lmtt sub-encoding to TS1/0 on input line 384.
|
||||
Package textcomp Info: Setting qhv sub-encoding to TS1/0 on input line 385.
|
||||
Package textcomp Info: Setting qag sub-encoding to TS1/0 on input line 386.
|
||||
Package textcomp Info: Setting qbk sub-encoding to TS1/0 on input line 387.
|
||||
Package textcomp Info: Setting qcr sub-encoding to TS1/0 on input line 388.
|
||||
Package textcomp Info: Setting qcs sub-encoding to TS1/0 on input line 389.
|
||||
Package textcomp Info: Setting qpl sub-encoding to TS1/0 on input line 390.
|
||||
Package textcomp Info: Setting qtm sub-encoding to TS1/0 on input line 391.
|
||||
Package textcomp Info: Setting qzc sub-encoding to TS1/0 on input line 392.
|
||||
Package textcomp Info: Setting qhvc sub-encoding to TS1/0 on input line 393.
|
||||
Package textcomp Info: Setting futs sub-encoding to TS1/4 on input line 394.
|
||||
Package textcomp Info: Setting futx sub-encoding to TS1/4 on input line 395.
|
||||
Package textcomp Info: Setting futj sub-encoding to TS1/4 on input line 396.
|
||||
Package textcomp Info: Setting hlh sub-encoding to TS1/3 on input line 397.
|
||||
Package textcomp Info: Setting hls sub-encoding to TS1/3 on input line 398.
|
||||
Package textcomp Info: Setting hlst sub-encoding to TS1/3 on input line 399.
|
||||
Package textcomp Info: Setting hlct sub-encoding to TS1/5 on input line 400.
|
||||
Package textcomp Info: Setting hlx sub-encoding to TS1/5 on input line 401.
|
||||
Package textcomp Info: Setting hlce sub-encoding to TS1/5 on input line 402.
|
||||
Package textcomp Info: Setting hlcn sub-encoding to TS1/5 on input line 403.
|
||||
Package textcomp Info: Setting hlcw sub-encoding to TS1/5 on input line 404.
|
||||
Package textcomp Info: Setting hlcf sub-encoding to TS1/5 on input line 405.
|
||||
Package textcomp Info: Setting pplx sub-encoding to TS1/3 on input line 406.
|
||||
Package textcomp Info: Setting pplj sub-encoding to TS1/3 on input line 407.
|
||||
Package textcomp Info: Setting ptmx sub-encoding to TS1/4 on input line 408.
|
||||
Package textcomp Info: Setting ptmj sub-encoding to TS1/4 on input line 409.
|
||||
)
|
||||
LaTeX Font Info: Redeclaring symbol font `letters' on input line 76.
|
||||
LaTeX Font Info: Encoding `OML' has changed to `LS1' for symbol font
|
||||
(Font) `letters' in the math version `normal' on input line 76.
|
||||
LaTeX Font Info: Overwriting symbol font `letters' in version `normal'
|
||||
(Font) OML/cmm/m/it --> LS1/stix/m/it on input line 76.
|
||||
LaTeX Font Info: Encoding `OML' has changed to `LS1' for symbol font
|
||||
(Font) `letters' in the math version `bold' on input line 76.
|
||||
LaTeX Font Info: Overwriting symbol font `letters' in version `bold'
|
||||
(Font) OML/cmm/b/it --> LS1/stix/m/it on input line 76.
|
||||
LaTeX Font Info: Redeclaring symbol font `operators' on input line 77.
|
||||
LaTeX Font Info: Encoding `OT1' has changed to `LS1' for symbol font
|
||||
(Font) `operators' in the math version `normal' on input line 77.
|
||||
LaTeX Font Info: Overwriting symbol font `operators' in version `normal'
|
||||
(Font) OT1/cmr/m/n --> LS1/stix/m/n on input line 77.
|
||||
LaTeX Font Info: Encoding `OT1' has changed to `LS1' for symbol font
|
||||
(Font) `operators' in the math version `bold' on input line 77.
|
||||
LaTeX Font Info: Overwriting symbol font `operators' in version `bold'
|
||||
(Font) OT1/cmr/bx/n --> LS1/stix/m/n on input line 77.
|
||||
\symbold-operators=\mathgroup6
|
||||
LaTeX Font Info: Redeclaring symbol font `symbols' on input line 79.
|
||||
LaTeX Font Info: Encoding `OMS' has changed to `LS1' for symbol font
|
||||
(Font) `symbols' in the math version `normal' on input line 79.
|
||||
LaTeX Font Info: Overwriting symbol font `symbols' in version `normal'
|
||||
(Font) OMS/cmsy/m/n --> LS1/stixscr/m/n on input line 79.
|
||||
LaTeX Font Info: Encoding `OMS' has changed to `LS1' for symbol font
|
||||
(Font) `symbols' in the math version `bold' on input line 79.
|
||||
LaTeX Font Info: Overwriting symbol font `symbols' in version `bold'
|
||||
(Font) OMS/cmsy/b/n --> LS1/stixscr/m/n on input line 79.
|
||||
\symsymbols2=\mathgroup7
|
||||
\symsymbols3=\mathgroup8
|
||||
\symsymbols4=\mathgroup9
|
||||
\symintegrals=\mathgroup10
|
||||
LaTeX Font Info: Redeclaring symbol font `largesymbols' on input line 84.
|
||||
LaTeX Font Info: Encoding `OMX' has changed to `LS2' for symbol font
|
||||
(Font) `largesymbols' in the math version `normal' on input line 8
|
||||
4.
|
||||
LaTeX Font Info: Overwriting symbol font `largesymbols' in version `normal'
|
||||
(Font) OMX/cmex/m/n --> LS2/stixex/m/n on input line 84.
|
||||
LaTeX Font Info: Encoding `OMX' has changed to `LS2' for symbol font
|
||||
(Font) `largesymbols' in the math version `bold' on input line 84.
|
||||
|
||||
LaTeX Font Info: Overwriting symbol font `largesymbols' in version `bold'
|
||||
(Font) OMX/cmex/m/n --> LS2/stixex/m/n on input line 84.
|
||||
\symarrows1=\mathgroup11
|
||||
\symarrows2=\mathgroup12
|
||||
\symarrows3=\mathgroup13
|
||||
LaTeX Font Info: Overwriting symbol font `letters' in version `bold'
|
||||
(Font) LS1/stix/m/it --> LS1/stix/b/it on input line 88.
|
||||
LaTeX Font Info: Overwriting symbol font `operators' in version `bold'
|
||||
(Font) LS1/stix/m/n --> LS1/stix/b/n on input line 89.
|
||||
LaTeX Font Info: Overwriting symbol font `symbols' in version `bold'
|
||||
(Font) LS1/stixscr/m/n --> LS1/stixscr/b/n on input line 90.
|
||||
LaTeX Font Info: Overwriting symbol font `symbols2' in version `bold'
|
||||
(Font) LS1/stixfrak/m/n --> LS1/stixfrak/b/n on input line 91.
|
||||
|
||||
LaTeX Font Info: Overwriting symbol font `symbols3' in version `bold'
|
||||
(Font) LS1/stixbb/m/n --> LS1/stixbb/b/n on input line 92.
|
||||
LaTeX Font Info: Overwriting symbol font `symbols4' in version `bold'
|
||||
(Font) LS1/stixbb/m/it --> LS1/stixbb/b/it on input line 93.
|
||||
LaTeX Font Info: Overwriting symbol font `integrals' in version `bold'
|
||||
(Font) LS2/stixcal/m/n --> LS2/stixcal/b/n on input line 94.
|
||||
LaTeX Font Info: Overwriting symbol font `largesymbols' in version `bold'
|
||||
(Font) LS2/stixex/m/n --> LS2/stixex/b/n on input line 95.
|
||||
LaTeX Font Info: Overwriting symbol font `arrows1' in version `bold'
|
||||
(Font) LS1/stixsf/m/n --> LS1/stixsf/b/n on input line 96.
|
||||
LaTeX Font Info: Overwriting symbol font `arrows2' in version `bold'
|
||||
(Font) LS1/stixsf/m/it --> LS1/stixsf/b/it on input line 97.
|
||||
LaTeX Font Info: Overwriting symbol font `arrows3' in version `bold'
|
||||
(Font) LS2/stixtt/m/n --> LS2/stixtt/b/n on input line 98.
|
||||
LaTeX Font Info: Redeclaring math alphabet \mathit on input line 99.
|
||||
LaTeX Font Info: Redeclaring math alphabet \mathfrak on input line 102.
|
||||
LaTeX Font Info: Redeclaring math alphabet \mathsf on input line 106.
|
||||
LaTeX Font Info: Redeclaring math alphabet \mathtt on input line 108.
|
||||
LaTeX Font Info: Redeclaring math alphabet \mathbf on input line 109.
|
||||
LaTeX Info: Redefining \yen on input line 456.
|
||||
LaTeX Info: Redefining \circledR on input line 458.
|
||||
LaTeX Info: Redefining \checkmark on input line 460.
|
||||
LaTeX Info: Redefining \maltese on input line 461.
|
||||
LaTeX Info: Redefining \vdots on input line 1518.
|
||||
LaTeX Info: Redefining \cdots on input line 1522.
|
||||
LaTeX Info: Redefining \not on input line 2144.
|
||||
) (./PLFA.aux)
|
||||
\openout1 = `PLFA.aux'.
|
||||
|
||||
LaTeX Font Info: Checking defaults for OML/cmm/m/it on input line 24.
|
||||
LaTeX Font Info: ... okay on input line 24.
|
||||
LaTeX Font Info: Checking defaults for T1/cmr/m/n on input line 24.
|
||||
LaTeX Font Info: ... okay on input line 24.
|
||||
LaTeX Font Info: Checking defaults for OT1/cmr/m/n on input line 24.
|
||||
LaTeX Font Info: ... okay on input line 24.
|
||||
LaTeX Font Info: Checking defaults for OMS/cmsy/m/n on input line 24.
|
||||
LaTeX Font Info: ... okay on input line 24.
|
||||
LaTeX Font Info: Checking defaults for OMX/cmex/m/n on input line 24.
|
||||
LaTeX Font Info: ... okay on input line 24.
|
||||
LaTeX Font Info: Checking defaults for U/cmr/m/n on input line 24.
|
||||
LaTeX Font Info: ... okay on input line 24.
|
||||
LaTeX Font Info: Checking defaults for T3/cmr/m/n on input line 24.
|
||||
LaTeX Font Info: Try loading font information for T3+cmr on input line 24.
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/tipa/t3cmr.fd
|
||||
File: t3cmr.fd 2001/12/31 TIPA font definitions
|
||||
)
|
||||
LaTeX Font Info: ... okay on input line 24.
|
||||
LaTeX Font Info: Checking defaults for TS1/cmr/m/n on input line 24.
|
||||
LaTeX Font Info: Try loading font information for TS1+cmr on input line 24.
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/ts1cmr.fd
|
||||
File: ts1cmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions
|
||||
)
|
||||
LaTeX Font Info: ... okay on input line 24.
|
||||
LaTeX Font Info: Checking defaults for LS1/stix/m/n on input line 24.
|
||||
LaTeX Font Info: Try loading font information for LS1+stix on input line 24.
|
||||
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stix.fd
|
||||
File: ls1stix.fd 2015/04/17 v1.1.2-latex STIX LS1 font definitions
|
||||
)
|
||||
LaTeX Font Info: ... okay on input line 24.
|
||||
LaTeX Font Info: Checking defaults for LS2/stix/m/n on input line 24.
|
||||
LaTeX Font Info: Try loading font information for LS2+stix on input line 24.
|
||||
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls2stix.fd
|
||||
File: ls2stix.fd 2015/04/17 v1.1.2-latex STIX LS2 font definitions
|
||||
)
|
||||
LaTeX Font Info: ... okay on input line 24.
|
||||
LaTeX Font Info: Try loading font information for T1+stix on input line 24.
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/stix/t1stix.fd
|
||||
File: t1stix.fd 2015/04/17 v1.1.2-latex STIX T1 font definitions
|
||||
)
|
||||
(/Users/wadler/Library/texmf/tex/latex/supp-pdf.tex
|
||||
[Loading MPS to PDF converter (version 2006.09.02).]
|
||||
\scratchcounter=\count129
|
||||
\scratchdimen=\dimen133
|
||||
\scratchbox=\box54
|
||||
\nofMPsegments=\count130
|
||||
\nofMParguments=\count131
|
||||
\MPscratchCnt=\count132
|
||||
\MPscratchDim=\dimen134
|
||||
\MPnumerator=\count133
|
||||
\everyMPtoPDFconversion=\toks28
|
||||
) (/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/ucsencs.def
|
||||
File: ucsencs.def 2011/01/21 Fixes to fontencodings LGR, T3
|
||||
T3\textscriptg already defined.
|
||||
|
||||
fontencoding T3 patched
|
||||
)
|
||||
LaTeX Font Info: Font shape `T1/stix/bx/n' in size <14.4> not available
|
||||
(Font) Font shape `T1/stix/b/n' tried instead on input line 30.
|
||||
LaTeX Font Info: Try loading font information for LS1+stixscr on input line
|
||||
30.
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stixscr.fd
|
||||
File: ls1stixscr.fd 2015/04/17 v1.1.2-latex STIX script LS1 font definitions
|
||||
)
|
||||
LaTeX Font Info: Try loading font information for LS2+stixex on input line 3
|
||||
0.
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls2stixex.fd
|
||||
File: ls2stixex.fd 2015/04/17 v1.1.2-latex STIX extentions LS2 font definitions
|
||||
|
||||
)
|
||||
LaTeX Font Info: Try loading font information for U+msa on input line 30.
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/umsa.fd
|
||||
File: umsa.fd 2013/01/14 v3.01 AMS symbols A
|
||||
)
|
||||
LaTeX Font Info: Try loading font information for U+msb on input line 30.
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/amsfonts/umsb.fd
|
||||
File: umsb.fd 2013/01/14 v3.01 AMS symbols B
|
||||
)
|
||||
LaTeX Font Info: Try loading font information for LS1+stixfrak on input line
|
||||
30.
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stixfrak.fd
|
||||
File: ls1stixfrak.fd 2015/04/17 v1.1.2-latex STIX fraktur LS1 font definitions
|
||||
)
|
||||
LaTeX Font Info: Try loading font information for LS1+stixbb on input line 3
|
||||
0.
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stixbb.fd
|
||||
File: ls1stixbb.fd 2015/04/17 v1.1.2-latex STIX blackboard LS1 font definitions
|
||||
|
||||
)
|
||||
LaTeX Font Info: Try loading font information for LS2+stixcal on input line
|
||||
30.
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls2stixcal.fd
|
||||
File: ls2stixcal.fd 2015/04/17 v1.1.2-latex STIX calligraphic LS2 font definiti
|
||||
ons
|
||||
)
|
||||
LaTeX Font Info: Try loading font information for LS1+stixsf on input line 3
|
||||
0.
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls1stixsf.fd
|
||||
File: ls1stixsf.fd 2015/04/17 v1.1.2-latex STIX sans-serif LS1 font definitions
|
||||
|
||||
)
|
||||
LaTeX Font Info: Try loading font information for LS2+stixtt on input line 3
|
||||
0.
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ls2stixtt.fd
|
||||
File: ls2stixtt.fd 2015/04/17 v1.1.2-latex STIX typewriter LS2 font definitions
|
||||
|
||||
)
|
||||
LaTeX Font Info: Try loading font information for T1+cmtt on input line 30.
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/base/t1cmtt.fd
|
||||
File: t1cmtt.fd 2014/09/29 v2.5h Standard LaTeX font definitions
|
||||
)
|
||||
LaTeX Font Info: Font shape `T1/stix/bx/n' in size <9> not available
|
||||
(Font) Font shape `T1/stix/b/n' tried instead on input line 32.
|
||||
|
||||
Overfull \hbox (1.0718pt too wide) in paragraph at lines 33--42
|
||||
[]\T1/stix/m/n/9 The lead-ing text-book for for-mal meth-ods is \T1/stix/m/it/9
|
||||
Soft-ware Foun-da-tions \T1/stix/m/n/9 (SF),
|
||||
[]
|
||||
|
||||
LaTeX Font Info: Try loading font information for TS1+stix on input line 61.
|
||||
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/stix/ts1stix.fd
|
||||
File: ts1stix.fd 2015/04/17 v1.1.2-latex STIX TS1 font definitions
|
||||
)
|
||||
LaTeX Font Info: Font shape `T1/stix/bx/n' in size <12> not available
|
||||
(Font) Font shape `T1/stix/b/n' tried instead on input line 64.
|
||||
[1
|
||||
|
||||
{/usr/local/texlive/2016/texmf-var/fonts/map/pdftex/updmap/pdftex.map}]
|
||||
Underfull \vbox (badness 3601) has occurred while \output is active []
|
||||
|
||||
[2]
|
||||
LaTeX Font Info: Font shape `T1/stix/bx/n' in size <10> not available
|
||||
(Font) Font shape `T1/stix/b/n' tried instead on input line 203.
|
||||
|
||||
[3]
|
||||
Overfull \hbox (5.29643pt too wide) in paragraph at lines 230--233
|
||||
\T1/stix/m/n/10 im-por-tant role in the sub-se-quent de-vel-op-ment. Also in-tr
|
||||
o-duces de-pen-dent records, lambda
|
||||
[]
|
||||
|
||||
[4] <figures/plfa-progress-1.png, id=21, 784.9325pt x 753.81625pt>
|
||||
File: figures/plfa-progress-1.png Graphic file (type png)
|
||||
|
||||
<use figures/plfa-progress-1.png> [5]
|
||||
<figures/plfa-progress-2.png, id=26, 783.92876pt x 509.905pt>
|
||||
File: figures/plfa-progress-2.png Graphic file (type png)
|
||||
|
||||
<use figures/plfa-progress-2.png>
|
||||
<figures/plfa-progress-3a.png, id=27, 784.9325pt x 590.205pt>
|
||||
File: figures/plfa-progress-3a.png Graphic file (type png)
|
||||
|
||||
<use figures/plfa-progress-3a.png>
|
||||
<figures/sf-progress-1.png, id=28, 809.0225pt x 753.81625pt>
|
||||
File: figures/sf-progress-1.png Graphic file (type png)
|
||||
|
||||
<use figures/sf-progress-1.png>
|
||||
<figures/sf-progress-2.png, id=29, 679.53876pt x 687.56876pt>
|
||||
File: figures/sf-progress-2.png Graphic file (type png)
|
||||
|
||||
<use figures/sf-progress-2.png> [6 <./figures/plfa-progress-1.png>] [7 <./figur
|
||||
es/plfa-progress-2.png> <./figures/plfa-progress-3a.png>] [8 <./figures/sf-prog
|
||||
ress-1.png>]
|
||||
Underfull \vbox (badness 10000) has occurred while \output is active []
|
||||
|
||||
[9 <./figures/sf-progress-2.png>]
|
||||
Underfull \vbox (badness 1102) has occurred while \output is active []
|
||||
|
||||
[10]
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/data/uni-32.def
|
||||
File: uni-32.def 2013/05/13 UCS: Unicode data U+2000..U+20FF
|
||||
)
|
||||
(/usr/local/texlive/2016/texmf-dist/tex/latex/ucs/data/uni-33.def
|
||||
File: uni-33.def 2013/05/13 UCS: Unicode data U+2100..U+21FF
|
||||
)
|
||||
<figures/plfa-eval.png, id=51, 623.32875pt x 753.81625pt>
|
||||
File: figures/plfa-eval.png Graphic file (type png)
|
||||
|
||||
<use figures/plfa-eval.png> [11] [12 <./figures/plfa-eval.png>] [13]
|
||||
(./PLFA.bbl [14] [15
|
||||
|
||||
]) [16] (./PLFA.aux) )
|
||||
Here is how much of TeX's memory you used:
|
||||
7316 strings out of 493014
|
||||
94897 string characters out of 6133352
|
||||
148843 words of memory out of 5000000
|
||||
10698 multiletter control sequences out of 15000+600000
|
||||
70168 words of font info for 102 fonts, out of 8000000 for 9000
|
||||
1141 hyphenation exceptions out of 8191
|
||||
42i,7n,37p,797b,384s stack positions out of 5000i,500n,10000p,200000b,80000s
|
||||
{/usr/local/texlive/2016/texmf-dist/fonts/enc/dvips/cm-su
|
||||
per/cm-super-t1.enc}{/usr/local/texlive/2016/texmf-dist/fonts/enc/dvips/stix/st
|
||||
ix-ts1.enc}{/usr/local/texlive/2016/texmf-dist/fonts/enc/dvips/stix/stix-t1.enc
|
||||
}</usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/STIXGeneral-Bold.p
|
||||
fb></usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/STIXGeneral-Ital
|
||||
ic.pfb></usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/STIXGeneral-
|
||||
Regular.pfb></usr/local/texlive/2016/texmf-dist/fonts/type1/public/cm-super/sft
|
||||
t0900.pfb></usr/local/texlive/2016/texmf-dist/fonts/type1/public/cm-super/sftt1
|
||||
000.pfb></usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/stix-mathfr
|
||||
ak.pfb></usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/stix-mathit.
|
||||
pfb></usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/stix-mathrm.pfb
|
||||
></usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/stix-mathsf.pfb></
|
||||
usr/local/texlive/2016/texmf-dist/fonts/type1/public/stix/stix-mathtt.pfb>
|
||||
Output written on PLFA.pdf (16 pages, 1193220 bytes).
|
||||
PDF statistics:
|
||||
114 PDF objects out of 1000 (max. 8388607)
|
||||
73 compressed objects within 1 object stream
|
||||
0 named destinations out of 1000 (max. 500000)
|
||||
31 words of extra memory for PDF output out of 10000 (max. 10000000)
|
||||
|
||||
|
Before Width: | Height: | Size: 168 KiB After Width: | Height: | Size: 168 KiB |
|
Before Width: | Height: | Size: 105 KiB After Width: | Height: | Size: 105 KiB |
|
Before Width: | Height: | Size: 120 KiB After Width: | Height: | Size: 120 KiB |
|
Before Width: | Height: | Size: 148 KiB After Width: | Height: | Size: 148 KiB |
|
Before Width: | Height: | Size: 208 KiB After Width: | Height: | Size: 208 KiB |
|
Before Width: | Height: | Size: 135 KiB After Width: | Height: | Size: 135 KiB |
|
Before Width: | Height: | Size: 25 KiB After Width: | Height: | Size: 25 KiB |
|
Before Width: | Height: | Size: 240 KiB After Width: | Height: | Size: 240 KiB |
|
Before Width: | Height: | Size: 275 KiB After Width: | Height: | Size: 275 KiB |
|
Before Width: | Height: | Size: 211 KiB After Width: | Height: | Size: 211 KiB |
|
Before Width: | Height: | Size: 473 KiB After Width: | Height: | Size: 473 KiB |
|
Before Width: | Height: | Size: 360 KiB After Width: | Height: | Size: 360 KiB |
|
Before Width: | Height: | Size: 334 KiB After Width: | Height: | Size: 334 KiB |
|
Before Width: | Height: | Size: 36 KiB After Width: | Height: | Size: 36 KiB |
|
Before Width: | Height: | Size: 379 KiB After Width: | Height: | Size: 379 KiB |
|
Before Width: | Height: | Size: 260 KiB After Width: | Height: | Size: 260 KiB |
|
Before Width: | Height: | Size: 86 KiB After Width: | Height: | Size: 86 KiB |
407
tspl/mock.tex
407
tspl/mock.tex
|
|
@ -1,407 +0,0 @@
|
|||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%
|
||||
% I N F O R M A T I C S
|
||||
% Honours Exam LaTeX Template for Exam Authors
|
||||
%
|
||||
% Created: 12-Oct-2009 by G.O.Passmore.
|
||||
% Last Updated: 10-Sep-2018 by I. Murray
|
||||
%
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
%%% The following define the status of the exam papers in the order
|
||||
%%% required. Simply remove the comment (i.e., the % symbol) just
|
||||
%%% before the appropriate one and comment the others out.
|
||||
|
||||
%\newcommand\status{\internal}
|
||||
%\newcommand\status{\external}
|
||||
\newcommand\status{\final}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
%%% The following three lines are always required. You may add
|
||||
%%% custom packages to the one already defined if necessary.
|
||||
|
||||
\documentclass{examhons2018}
|
||||
\usepackage{amssymb}
|
||||
\usepackage{amsmath}
|
||||
\usepackage{semantic}
|
||||
\usepackage{stix}
|
||||
|
||||
%%% Uncomment the \checkmarksfalse line if the macros that check the
|
||||
%%% mark totals cause problems. However, please do not make your
|
||||
%%% questions add up to a non-standard number of marks without
|
||||
%%% permission of the convenor.
|
||||
%\checkmarksfalse
|
||||
|
||||
\begin{document}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%
|
||||
% Replace {ad} below with the ITO code for your course. This will
|
||||
% be used by the ITO LaTeX installation to install course-specific
|
||||
% data into the exam versions it produces from this document.
|
||||
%
|
||||
% Your choices are (in course title order):
|
||||
%
|
||||
% {anlp} - Acc. Natural Language Processing (MSc)
|
||||
% {aleone} - Adaptive Learning Environments 1 (Inf4)
|
||||
% {adbs} - Advanced Databases (Inf4)
|
||||
% {av} - Advanced Vision (Inf4)
|
||||
% {av-dl} - Advanced Vision - distance learning (MSc)
|
||||
% {apl} - Advances in Programming Languages (Inf4)
|
||||
% {abs} - Agent Based Systems [L10] (Inf3)
|
||||
% {afds} - Algorithmic Foundations of Data Science (MSc)
|
||||
% {agta} - Algorithmic Game Theory and its Apps. (MSc)
|
||||
% {ads} - Algorithms and Data Structures (Inf3)
|
||||
% {ad} - Applied Databases (MSc)
|
||||
% {aipf} - Artificial Intelligence Present and Future (MSc)
|
||||
% {ar} - Automated Reasoning (Inf3)
|
||||
% {asr} - Automatic Speech Recognition (Inf4)
|
||||
% {bioone} - Bioinformatics 1 (MSc)
|
||||
% {biotwo} - Bioinformatics 2 (MSc)
|
||||
% {bdl} - Blockchains and Distributed Ledgers (Inf4)
|
||||
% {cqi} - Categories and Quantum Informatics (MSc)
|
||||
% {copt} - Compiler Opimisation [L11] (Inf4)
|
||||
% {ct} - Compiling Techniques (Inf3)
|
||||
% {ccs} - Computational Cognitive Science (Inf3)
|
||||
% {cmc} - Computational Complexity (Inf4)
|
||||
% {ca} - Computer Algebra (Inf4)
|
||||
% {cav} - Computer Animation and Visualisation (Inf4)
|
||||
% {car} - Computer Architecture (Inf3)
|
||||
% {comn} - Computer Comms. and Networks (Inf3)
|
||||
% {cd} - Computer Design (Inf3)
|
||||
% {cg} - Computer Graphics [L11] (Inf4)
|
||||
% {cn} - Computer Networking [L11] (Inf4)
|
||||
% {cp} - Computer Prog. Skills and Concepts (nonhons)
|
||||
% {cs} - Computer Security (Inf3)
|
||||
% {dds} - Data, Design and Society (nonhons)
|
||||
% {dme} - Data Mining and Exploration (Msc)
|
||||
% {dbs} - Database Systems (Inf3)
|
||||
% {dmr} - Decision Making in Robots and Autonomous Agents(MSc)
|
||||
% {dmmr} - Discrete Maths. and Math. Reasoning (nonhons)
|
||||
% {ds} - Distributed Systems [L11] (Inf4)
|
||||
% {epl} - Elements of Programming Languages (Inf3)
|
||||
% {es} - Embedded Software (Inf4)
|
||||
% {exc} - Extreme Computing (Inf4)
|
||||
% {fv} - Formal Verification (Inf4)
|
||||
% {fnlp} - Foundations of Natural Language Processing (Inf3)
|
||||
% {hci} - Human-Computer Interaction [L11] (Inf4)
|
||||
% {infonea} - Informatics 1 - Introduction to Computation(nonhons)
|
||||
% different sittings for INF1A programming exams
|
||||
% {infoneapone} - Informatics 1 - Introduction to Computation(nonhons)
|
||||
% {infoneaptwo} - Informatics 1 - Introduction to Computation(nonhons)
|
||||
% {infoneapthree} - Informatics 1 - Introduction to Computation(nonhons)
|
||||
% {infonecg} - Informatics 1 - Cognitive Science (nonhons)
|
||||
% {infonecl} - Informatics 1 - Computation and Logic (nonhons)
|
||||
% {infoneda} - Informatics 1 - Data and Analysis (nonhons)
|
||||
% {infonefp} - Informatics 1 - Functional Programming (nonhons)
|
||||
% If there are two sittings of FP, use infonefpam for the first
|
||||
% paper and infonefppm for the second sitting.
|
||||
% {infoneop} - Informatics 1 - Object-Oriented Programming(nonhons)
|
||||
% If there are two sittings of OOP, use infoneopam for the first
|
||||
% paper and infoneoppm for the second sitting.
|
||||
% {inftwoa} - Informatics 2A: Proc. F&N Languages (nonhons)
|
||||
% {inftwob} - Informatics 2B: Algs., D.Structs., Learning(nonhons)
|
||||
% {inftwoccs}- Informatics 2C-CS: Computer Systems (nonhons)
|
||||
% {inftwocse}- Informatics 2C: Software Engineering (nonhons)
|
||||
% {inftwod} - Informatics 2D: Reasoning and Agents (nonhons)
|
||||
% {iar} - Intelligent Autonomous Robotics (Inf4)
|
||||
% {it} - Information Theory (MSc)
|
||||
% {imc} - Introduction to Modern Cryptography (Inf4)
|
||||
% {iotssc} - Internet of Things, Systems, Security and the Cloud (Inf4)
|
||||
% (iqc) - Introduction to Quantum Computing (Inf4)
|
||||
% (itcs) - Introduction to Theoretical Computer Science (Inf3)
|
||||
% {ivc} - Image and Vision Computing (MSc)
|
||||
% {ivr} - Introduction to Vision and Robotics (Inf3)
|
||||
% {ivr-dl} - Introduction to Vision and Robotics - distance learning (Msc)
|
||||
% {iaml} - Introductory Applied Machine Learning (MSc)
|
||||
% {iaml-dl} - Introductory Applied Machine Learning - distance learning (MSc)
|
||||
% {lpt} - Logic Programming - Theory (Inf3)
|
||||
% {lpp} - Logic Programming - Programming (Inf3)
|
||||
% {mlpr} - Machine Learning & Pattern Recognition (Inf4)
|
||||
% {mt} - Machine Translation (Inf4)
|
||||
% {mi} - Music Informatics (MSc)
|
||||
% {nlu} - Natural Language Understanding [L11] (Inf4)
|
||||
% {nc} - Neural Computation (MSc)
|
||||
% {nat} - Natural Computing (MSc)
|
||||
% {nluplus} - Natural Language Understanding, Generation, and Machine Translation(MSc)
|
||||
% {nip} - Neural Information Processing (MSc)
|
||||
% {os} - Operating Systems (Inf3)
|
||||
% {pa} - Parallel Architectures [L11] (Inf4)
|
||||
% {pdiot} - Principles and Design of IoT Systems (Inf4)
|
||||
% {ppls} - Parallel Prog. Langs. and Sys. [L11] (Inf4)
|
||||
% {pm} - Performance Modelling (Inf4)
|
||||
% {pmr} - Probabilistic Modelling and Reasoning (MSc)
|
||||
% {pi} - Professional Issues (Inf3)
|
||||
% {rc} - Randomness and Computation (Inf4)
|
||||
% {rl} - Reinforcement Learning (MSc)
|
||||
% {rlsc} - Robot Learning and Sensorimotor Control (MSc)
|
||||
% {rss} - Robotics: Science and Systems (MSc)
|
||||
% {sp} - Secure Programming (Inf4)
|
||||
% {sws} - Semantic Web Systems (Inf4)
|
||||
% {stn} - Social and Technological Networks (Inf4)
|
||||
% {sapm} - Software Arch., Proc. and Mgmt. [L11] (Inf4)
|
||||
% {sdm} - Software Design and Modelling (Inf3)
|
||||
% {st} - Software Testing (Inf3)
|
||||
% {ttds} - Text Technologies for Data Science (Inf4)
|
||||
% {tspl} - Types and Semantics for Programming Langs. (Inf4)
|
||||
% {usec} - Usable Security and Privacy (Inf4)
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
\setcourse{tspl}
|
||||
\initcoursedata
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%
|
||||
% Set your exam rubric type.
|
||||
%
|
||||
% Most courses in the School have exams that add up to 50 marks,
|
||||
% and your choices are:
|
||||
% {qu1_and_either_qu2_or_qu3, any_two_of_three, do_exam}
|
||||
% (which include the "CALCULATORS MAY NOT BE USED..." text), or
|
||||
% {qu1_and_either_qu2_or_qu3_calc, any_two_of_three_calc, do_exam_calc}
|
||||
% (which DO NOT include the "CALCULATORS MAY NOT BE USED..." text), or
|
||||
% {custom}.
|
||||
%
|
||||
% Note, if you opt to create a custom rubric, you must:
|
||||
%
|
||||
% (i) **have permission** from the appropriate authority, and
|
||||
% (ii) execute:
|
||||
%
|
||||
% \setrubrictype{} to specify the custom rubric information.
|
||||
%
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
\setrubric{qu1_and_either_qu2_or_qu3}
|
||||
|
||||
\examtitlepage
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%
|
||||
% Manual override for total page number computation.
|
||||
%
|
||||
% As long as you run latex upon this document three times in a row,
|
||||
% the right number of `total pages' should be computed and placed
|
||||
% in the footer of all pages except the title page.
|
||||
%
|
||||
% But, if this fails, you can set that number yourself with the
|
||||
% following command:
|
||||
%
|
||||
% \settotalpages{n} with n a natural number.
|
||||
%
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%
|
||||
% Beginning of your exam text.
|
||||
%
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
\begin{enumerate}
|
||||
|
||||
\item \rubricqA
|
||||
|
||||
\newcommand{\key}{\texttt}
|
||||
\newcommand{\List}{\key{list}}
|
||||
\newcommand{\nil}{\texttt{[]}}
|
||||
\newcommand{\cons}{\mathbin{\key{::}}}
|
||||
\newcommand{\member}{\key{member}}
|
||||
\newcommand{\sublist}{\key{sublist}}
|
||||
|
||||
This question uses the library definition of $\List$ in Agda.
|
||||
Here is an informal definition of the predicates $\in$
|
||||
and $\subseteq$. (In Emacs, you can type $\in$ as \verb$\in$ and $\subseteq$ as \verb$\subseteq$.)
|
||||
$\subseteq$
|
||||
\begin{gather*}
|
||||
\inference[$\key{here}$]
|
||||
{}
|
||||
{x \in (x \cons xs)}
|
||||
\qquad
|
||||
\inference[$\key{there}$]
|
||||
{x \in ys}
|
||||
{x \in (y \cons ys)}
|
||||
\\~\\
|
||||
\inference[$\key{done}$]
|
||||
{}
|
||||
{\nil \subseteq ys}
|
||||
\\~\\
|
||||
\inference[$\key{keep}$]
|
||||
{xs \subseteq ys}
|
||||
{(x \cons xs) \subseteq (x \cons ys)}
|
||||
\qquad
|
||||
\inference[$\key{drop}$]
|
||||
{xs \subseteq ys}
|
||||
{xs \subseteq (y \cons ys)}
|
||||
\end{gather*}
|
||||
|
||||
\begin{itemize}
|
||||
|
||||
\item[(a)] Formalise the definition above.
|
||||
\marks{10}
|
||||
|
||||
\item[(b)] Prove each of the following.
|
||||
\begin{itemize}
|
||||
\item[(i)] $\key{2} \in \key{[1,2,3]}$
|
||||
\item[(ii)] $\key{[1,3]} \subseteq \key{[1,2,3,4]}$
|
||||
\end{itemize}
|
||||
\marks{5}
|
||||
|
||||
\item[(c)] Prove the following.
|
||||
\begin{center}
|
||||
If $xs \subseteq ys$ then $z \in xs$ implies $z \in ys$ for all $z$.
|
||||
\end{center}
|
||||
\marks{10}
|
||||
|
||||
\end{itemize}
|
||||
|
||||
\newpage
|
||||
|
||||
\item \rubricqB
|
||||
|
||||
\newcommand{\Tree}{\texttt{Tree}}
|
||||
\newcommand{\leaf}{\texttt{leaf}}
|
||||
\newcommand{\branch}{\texttt{branch}}
|
||||
\newcommand{\CASET}{\texttt{caseT}}
|
||||
\newcommand{\caseT}[6]{\texttt{case}~#1~\texttt{[leaf}~#2~\Rightarrow~#3~\texttt{|}~#4~\texttt{branch}~#5~\Rightarrow~#6\texttt{]}}
|
||||
\newcommand{\ubar}{\texttt{\underline{~}}}
|
||||
\newcommand{\comma}{\,\texttt{,}\,}
|
||||
\newcommand{\V}{\texttt{V}}
|
||||
\newcommand{\dash}{\texttt{-}}
|
||||
\newcommand{\Value}{\texttt{Value}}
|
||||
\newcommand{\becomes}{\longrightarrow}
|
||||
\newcommand{\subst}[3]{#1~\texttt{[}~#2~\texttt{:=}~#3~\texttt{]}}
|
||||
|
||||
|
||||
You will be provided with a definition of intrinsically-typed lambda
|
||||
calculus in Agda. Consider constructs satisfying the following rules,
|
||||
written in extrinsically-typed style.
|
||||
|
||||
Typing:
|
||||
\begin{gather*}
|
||||
\inference[\leaf]
|
||||
{\Gamma \vdash M \typecolon A}
|
||||
{\Gamma \vdash \leaf~M \typecolon \Tree~A}
|
||||
\quad
|
||||
\inference[\branch]
|
||||
{\Gamma \vdash M \typecolon \Tree~A \\
|
||||
\Gamma \vdash N \typecolon \Tree~A}
|
||||
{\Gamma \vdash M~\branch~N \typecolon \Tree~A}
|
||||
\\~\\
|
||||
\inference[\CASET]
|
||||
{\Gamma \vdash L \typecolon \Tree~A \\
|
||||
\Gamma \comma x \typecolon A \vdash M \typecolon B \\
|
||||
\Gamma \comma y \typecolon \Tree~A \comma z \typecolon \Tree~A \vdash N \typecolon B}
|
||||
{\Gamma \vdash \caseT{L}{x}{M}{y}{z}{N} \typecolon B}
|
||||
\end{gather*}
|
||||
|
||||
Values:
|
||||
\begin{gather*}
|
||||
\inference[\V\dash\leaf]
|
||||
{\Value~V}
|
||||
{\Value~(\leaf~V)}
|
||||
\qquad
|
||||
\inference[\V\dash\branch]
|
||||
{\Value~V \\
|
||||
\Value~W}
|
||||
{\Value~(V~\branch~W)}
|
||||
\end{gather*}
|
||||
|
||||
Reduction:
|
||||
\begin{gather*}
|
||||
\inference[$\xi\dash\leaf$]
|
||||
{M \becomes M'}
|
||||
{\leaf{M} \becomes \leaf{M'}}
|
||||
\\~\\
|
||||
\inference[$\xi\dash\branch_1$]
|
||||
{M \becomes M'}
|
||||
{M~\branch~N \becomes M'~\branch~N}
|
||||
\qquad
|
||||
\inference[$\xi\dash\branch_2$]
|
||||
{\Value~V \\
|
||||
N \becomes N'}
|
||||
{V~\branch~N \becomes V~\branch~N'}
|
||||
\\~\\
|
||||
\inference[$\xi\dash\CASET$]
|
||||
{L \becomes L'}
|
||||
{\begin{array}{c}
|
||||
\caseT{L}{x}{M}{y}{z}{N} \becomes \\
|
||||
{} \quad \caseT{L'}{x}{M}{y}{z}{N}
|
||||
\end{array}}
|
||||
\\~\\
|
||||
\inference[$\beta\dash\leaf$]
|
||||
{\Value~V}
|
||||
{\caseT{(\leaf~V)}{x}{M}{y}{z}{N} \becomes \subst{M}{x}{V}}
|
||||
\\~\\
|
||||
\inference[$\beta\dash\branch$]
|
||||
{\Value~V \\
|
||||
\Value~W}
|
||||
{\caseT{(V~\branch~W)}{x}{M}{y}{z}{N} \becomes \subst{\subst{N}{y}{V}}{z}{W}}
|
||||
\end{gather*}
|
||||
|
||||
\begin{enumerate}
|
||||
\item[(a)] Extend the given definition to formalise the evaluation and
|
||||
typing rules, including any other required definitions.
|
||||
\marks{12}
|
||||
|
||||
\item[(b)] Prove progress. You will be provided with a proof of
|
||||
progress for the simply-typed lambda calculus that you may
|
||||
extend.
|
||||
\marks{13}
|
||||
\end{enumerate}
|
||||
|
||||
Please delimit any code you add as follows.
|
||||
\begin{verbatim}
|
||||
-- begin
|
||||
-- end
|
||||
\end{verbatim}
|
||||
|
||||
\newpage
|
||||
|
||||
\item \rubricqC
|
||||
|
||||
\newcommand{\Lift}{\texttt{Lift}}
|
||||
\newcommand{\delay}{\texttt{delay}}
|
||||
\newcommand{\force}{\texttt{force}}
|
||||
\newcommand{\up}{\uparrow}
|
||||
\newcommand{\dn}{\downarrow}
|
||||
|
||||
You will be provided with a definition of inference for extrinsically-typed lambda
|
||||
calculus in Agda. Consider constructs satisfying the following rules,
|
||||
written in extrinsically-typed style that support bidirectional inference.
|
||||
|
||||
Typing:
|
||||
\begin{gather*}
|
||||
\inference[$\delay$]
|
||||
{\Gamma \vdash M \dn A}
|
||||
{\Gamma \vdash \delay~M \dn \Lift~A}
|
||||
\\~\\
|
||||
\inference[$\force$]
|
||||
{\Gamma \vdash L \up \Lift~A}
|
||||
{\Gamma \vdash \force~L \up A}
|
||||
\end{gather*}
|
||||
|
||||
\begin{enumerate}
|
||||
\item[(a)] Extend the given definition to formalise the typing rules,
|
||||
and update the definition of equality on types.
|
||||
\marks{10}
|
||||
|
||||
\item[(b)] Extend the code to support type inference for the new features.
|
||||
\marks{15}
|
||||
\end{enumerate}
|
||||
|
||||
Please delimit any code you add as follows.
|
||||
\begin{verbatim}
|
||||
-- begin
|
||||
-- end
|
||||
\end{verbatim}
|
||||
|
||||
\end{enumerate}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%
|
||||
% End of your exam text.
|
||||
%
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
\end{document}
|
||||
Binary file not shown.
Loading…
Reference in a new issue