%% For double-blind review submission, w/o CCS and ACM Reference (max submission space)
% \documentclass[sigplan,10pt,review]{acmart}
% \settopmatter{printfolios=true,printccs=false,printacmref=false}
%% For double-blind review submission, w/ CCS and ACM Reference
%\documentclass[sigplan,review,anonymous]{acmart}\settopmatter{printfolios=true}
%% For single-blind review submission, w/o CCS and ACM Reference (max submission space)
%\documentclass[sigplan,review]{acmart}\settopmatter{printfolios=true,printccs=false,printacmref=false}
%% For single-blind review submission, w/ CCS and ACM Reference
%\documentclass[sigplan,review]{acmart}\settopmatter{printfolios=true}
%% For final camera-ready submission, w/ required CCS and ACM Reference
\documentclass[sigplan,screen]{acmart}\settopmatter{}


%% Conference information
%% Supplied to authors by publisher for camera-ready submission;
%% use defaults for review submission.

% \startPage{1}

%% Copyright information
%% Supplied to authors (based on authors' rights management selection;
%% see authors.acm.org) by publisher for camera-ready submission;
%% use 'none' for review submission.


%% Bibliography style
\bibliographystyle{ACM-Reference-Format}
%% Citation style
%  \citestyle{acmauthoryear}  %% For author/year citations
 \citestyle{acmnumeric}     %% For numeric citations
%\setcitestyle{nosort}      %% With 'acmnumeric', to disable automatic
                            %% sorting of references within a single citation;
                            %% e.g., \cite{Smith99,Carpenter05,Baker12}
                            %% rendered as [14,5,2] rather than [2,5,14].
%\setcitesyle{nocompress}   %% With 'acmnumeric', to disable automatic
                            %% compression of sequential references within a
                            %% single citation;
                            %% e.g., \cite{Baker12,Baker14,Baker16}
                            %% rendered as [2,3,4] rather than [2-4].


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Note: Authors migrating a paper from traditional SIGPLAN
%% proceedings format to PACMPL format must update the
%% '\documentclass' and topmatter commands above; see
%% 'acmart-pacmpl-template.tex'.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%% Some recommended packages.
\usepackage{booktabs}   %% For formal tables:
                        %% http://ctan.org/pkg/booktabs
\usepackage{subcaption} %% For complex figures with subfigures/subcaptions
                        %% http://ctan.org/pkg/subcaption


\begin{document}

%% Title information
\title[POPLMark Reloaded]{POPLMark Reloaded}         %% [Short Title] is optional;
                                        %% when present, will be used in
                                        %% header instead of Full Title.
% \titlenote{with title note}             %% \titlenote is optional;
                                        %% can be repeated if necessary;
                                        %% contents suppressed with 'anonymous'
 \subtitle{Mechanizing Logical Relations Proofs \\ (Invited Talk) }                     %% \subtitle is optional
% \subtitlenote{Invited talk}       %% \subtitlenote is optional;
                                        %% can be repeated if necessary;
                                        %% contents suppressed with 'anonymous'


%% Author information
%% Contents and number of authors suppressed with 'anonymous'.
%% Each author should be introduced by \author, followed by
%% \authornote (optional), \orcid (optional), \affiliation, and
%% \email.
%% An author may have multiple affiliations and/or emails; repeat the
%% appropriate command.
%% Many elements are not rendered, but should be provided for metadata
%% extraction tools.

%% Author with single affiliation.
\author{Brigitte Pientka}
% \authornote{with author1 note}          %% \authornote is optional;
                                          %% can be repeated if necessary
\orcid{nnnn-nnnn-nnnn-nnnn}               %% \orcid is optional
\affiliation{
%  \position{Position1}
%  \department{School of Computer Science}              %% \department is recommended
  \institution{McGill University}            %% \institution is required
%  \streetaddress{Street1 Address1}
   \city{Montreal}
  \state{QC}
  \country{Canada}                    %% \country is recommended
}
\email{bpientka@cs.mcgill.ca}          %% \email is recommended


%% Abstract
% Note: \begin{abstract}...\end{abstract} environment must come
%% before \maketitle command
 \begin{abstract}

Mechanizing formal systems, given via axioms and inference rules,
together with proofs about them plays an important role in 
establishing trust in formal developments. Over the past decade, the
POPLMark challenge \citep{Aydemir05TPHOLs} popularized the use of proof assistants in
mechanizing the metatheory of programming languages. Focusing on the the meta-theory of
$\mathtt{F_{<:}}$, it allowed the programming languages community to
survey existing techniques to represent and reason about syntactic
structures with binders and promote the use of proof
assistants. Today, mechanizing proofs is a
stable fixture in the daily life of programming languages
researchers. 

As a follow-up to the POPLMark Challenge, we propose a new collection of
benchmarks that use proofs by logical relations. Such proofs are now used to attack
problems in the theory of complex languages models, with applications
to issues in equivalence of programs, {compiler correctness},
representation independence and even more intensional 
properties such as non-interference, differential privacy and secure
multi-language inter-operability (see for example
~\citep{Ahmed15,BowmanA15,NeisHKMDV15}). Yet, they remain challenging
to mechanize.
 
% The goal of these benchmarks  is to better
% understand how to factor out a generic infrastructure for
% common and recurring issues beyond representing variables and achieve
% mechanized proofs that are more readable and easier to maintain. We see
% this not merely as an engineering challenge, but hope these
% benchmarks highlight the difficulties in mechanizing such proofs and also
% lead to cross-fertilization between general proof environments such as
% Coq, Agda or Isabelle on the one hand and specialized frameworks such
% as Abella and Beluga that target representing and reasoning about
% structures with binders on the other hand. 

% This eliminates the potential for mistakes in building up
% the primitive infrastructure and more importantly it lies the ground for
% representing proofs compactly and automating proofs efficiently, since
% the search space concentrates on essential parts and does not get
% bogged in the quagmire of bureaucratic details. 


In this talk, we
focus on one particular challenge problem, namely strong normalization
of a simply-typed lambda-calculus with a proof by Kripke-style logical
relations. We will advocate a modern view of this well-understood
problem by formulating our logical relation on well-typed terms. 
% This
% focus on reasoning about well-typed terms necessitates reasoning about
% Kripke-style context extensions. 
Using this case study, we share some
of the lessons learned tackling this challenge problem in Beluga \cite{PientkaC15}, a
proof environment that supports higher-order abstract syntax
encodings, first-class context and first-class substitutions. {We also
discuss and highlight similarities, strategies, and limitations 
% \newline
in other proof assistants when tackling this challenge problem.}
% %
% \newline\indent

We hope others will be motivated to submit solutions! The goal of this
talk is to engage the community in discussions on what support in
proof environments is needed to truly bring mechanized metatheory to
the masses.
\end{abstract}


%%% The following is specific to CPP'18 and the paper
%%% 'POPLMark Reloaded: Mechanizing Logical Relations Proofs (Invited Talk)'
%%% by Brigitte Pientka.
%%%
\setcopyright{rightsretained}
\acmPrice{15.00}
\acmDOI{10.1145/3167102}
\acmYear{2018}
\copyrightyear{2018}
\acmISBN{978-1-4503-5586-5/18/01}
\acmConference[CPP'18]{7th ACM SIGPLAN International Conference on Certified Programs and Proofs}{January 8--9, 2018}{Los Angeles, CA, USA}



%% 2012 ACM Computing Classification System (CSS) concepts
%% Generate at 'http://dl.acm.org/ccs/ccs.cfm'.
 \begin{CCSXML}
<ccs2012>
<concept>
<concept_id>10003752.10003790.10002990</concept_id>
<concept_desc>Theory of computation~Logic and verification</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10003752.10003790.10011740</concept_id>
<concept_desc>Theory of computation~Type theory</concept_desc>
<concept_significance>500</concept_significance>
</concept>
<concept>
<concept_id>10003752.10003790.10003794</concept_id>
<concept_desc>Theory of computation~Automated reasoning</concept_desc>
<concept_significance>300</concept_significance>
</concept>
<concept>
<concept_id>10011007.10011006.10011008.10011024.10011038</concept_id>
<concept_desc>Software and its engineering~Frameworks</concept_desc>
<concept_significance>300</concept_significance>
</concept>
<concept>
<concept_id>10011007.10011006.10011039.10011040</concept_id>
<concept_desc>Software and its engineering~Syntax</concept_desc>
<concept_significance>300</concept_significance>
</concept>
<concept>
<concept_id>10011007.10011006.10011039.10011311</concept_id>
<concept_desc>Software and its engineering~Semantics</concept_desc>
<concept_significance>300</concept_significance>
</concept>
</ccs2012>
\end{CCSXML}

\ccsdesc[500]{Theory of computation~Logic and verification}
\ccsdesc[500]{Theory of computation~Type theory}
\ccsdesc[300]{Theory of computation~Automated reasoning}
\ccsdesc[300]{Software and its engineering~Frameworks}
\ccsdesc[300]{Software and its engineering~Syntax}
\ccsdesc[300]{Software and its engineering~Semantics}
%% End of generated code


%% Keywords
%% comma separated list
\keywords{Mechanizing Metatheory, Logical Frameworks, Proof Assistants}  %% \keywords are mandatory in final camera-ready submission


 \maketitle
%% Note: \maketitle command must come after title commands, author
%% commands, abstract environment, Computing Classification System
%% environment and commands, and keywords command.


%% Acknowledgments
\begin{acks}       
This is joint work with Andreas Abel, Aliya Hameer, Alberto Momigliano, Kathrin
Stark, and Steven Schaefer.                     %% acks environment is optional
                                        %% contents suppressed with 'anonymous'
  %% Commands \grantsponsor{<sponsorID>}{<name>}{<url>} and
  %% \grantnum[<url>]{<sponsorID>}{<number>} should be used to
  %% acknowledge financial support and will be used by metadata
  %% extraction tools.
  This material is based upon work supported by the
  \grantsponsor{GS100000001}{Natural Sciences and Engineering Research
    Council (NSERC) of Canada}{http://dx.doi.org/10.13039/100000001}.
%  under Grant
%  No.~\grantnum{206263}{206263}.  
% Any opinions, findings, and
%  conclusions or recommendations expressed in this material are those
%  of the author and do not necessarily reflect the views of NSERC.
\end{acks}


%% Bibliography
 \bibliography{cpp}

%% Appendix
% \appendix
% \section{Appendix}

% Text of appendix \ldots

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
