246 lines
12 KiB
HTML
246 lines
12 KiB
HTML
<!DOCTYPE html>
|
|
<html lang="en"><head>
|
|
<meta charset="utf-8">
|
|
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
|
<meta name="viewport" content="width=device-width, initial-scale=1">
|
|
<title>Acknowledgements | Programming Language Foundations in Agda
|
|
</title><!-- Begin Jekyll SEO tag v2.6.1 -->
|
|
<meta name="generator" content="Jekyll v3.9.0" />
|
|
<meta property="og:title" content="Acknowledgements" />
|
|
<meta property="og:locale" content="en_US" />
|
|
<meta name="description" content="Programming Language Foundations in Agda" />
|
|
<meta property="og:description" content="Programming Language Foundations in Agda" />
|
|
<link rel="canonical" href="https://plfa.github.io/19.08/Acknowledgements/" />
|
|
<meta property="og:url" content="https://plfa.github.io/19.08/Acknowledgements/" />
|
|
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
|
|
<script type="application/ld+json">
|
|
{"url":"https://plfa.github.io/19.08/Acknowledgements/","headline":"Acknowledgements","description":"Programming Language Foundations in Agda","@type":"WebPage","@context":"https://schema.org"}</script>
|
|
<!-- End Jekyll SEO tag -->
|
|
<link rel="stylesheet" href="/19.08/assets/main.css"></head>
|
|
<body><header class="site-header" role="banner">
|
|
|
|
<div class="wrapper">
|
|
|
|
<a class="site-title" href="/19.08/">Programming Language Foundations in Agda
|
|
</a>
|
|
|
|
<nav class="site-nav">
|
|
<span class="menu-icon">
|
|
<svg viewBox="0 0 18 15" width="18px" height="15px">
|
|
<path fill="#424242" d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.031C17.335,0,18,0.665,18,1.484L18,1.484z"/>
|
|
<path fill="#424242" d="M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0c0-0.82,0.665-1.484,1.484-1.484 h15.031C17.335,6.031,18,6.696,18,7.516L18,7.516z"/>
|
|
<path fill="#424242" d="M18,13.516C18,14.335,17.335,15,16.516,15H1.484C0.665,15,0,14.335,0,13.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.031C17.335,12.031,18,12.696,18,13.516L18,13.516z"/>
|
|
</svg>
|
|
</span>
|
|
|
|
<div class="trigger">
|
|
<a class="page-link" href="/19.08/">The Book</a>
|
|
<a class="page-link" href="/19.08/Announcements/">Announcements</a>
|
|
<a class="page-link" href="/19.08/GettingStarted/">Getting Started</a>
|
|
<a class="page-link" href="/19.08/Citing/">Citing</a>
|
|
<a class="page-link" href="https://agda-zh.github.io/PLFA-zh/">中文</a>
|
|
</div>
|
|
</nav>
|
|
|
|
</div>
|
|
|
|
</header>
|
|
<main class="page-content" aria-label="Content">
|
|
<div class="wrapper">
|
|
<article class="post">
|
|
|
|
<header class="post-header">
|
|
<h1 class="post-title">Acknowledgements</h1>
|
|
</header>
|
|
|
|
<p style="text-align:center;">
|
|
|
|
<a alt="Previous chapter" href="/19.08/Untyped/">Prev</a>
|
|
|
|
|
|
•
|
|
|
|
|
|
|
|
|
|
<a alt="Next chapter" href="/19.08/Fonts/">Next</a>
|
|
|
|
</p>
|
|
|
|
|
|
<div class="post-content">
|
|
<p>Thank you to:</p>
|
|
<ul>
|
|
<li>The inventors of Agda, for a new playground.</li>
|
|
<li>The authors of Software Foundations, for inspiration.</li>
|
|
</ul>
|
|
|
|
<p>A special thank you, for inventing ideas on which
|
|
this book is based, and for hand-holding:</p>
|
|
<ul>
|
|
<li>Conor McBride</li>
|
|
<li>James McKinna</li>
|
|
<li>Ulf Norell</li>
|
|
<li>Andreas Abel</li>
|
|
</ul>
|
|
|
|
<p>For a note showing how much more compact it is to avoid raw terms:</p>
|
|
<ul>
|
|
<li>David Darais</li>
|
|
</ul>
|
|
|
|
<p><span class="force-end-of-list"></span>For pull requests big and small, and for answering questions on the Agda mailing list:</p>
|
|
<ul class="list-of-contributors"><li><a href="https://github.com/mdimjasevic">Marko Dimjašević</a></li><li><a href="https://github.com/Kwezan">Zbigniew Stanasiuk</a></li><li><a href="https://github.com/h4iku">Reza Gharibi</a></li><li><a href="https://github.com/ywata">Yasu Watanabe</a></li><li><a href="https://github.com/Cubesoup">Chad Nester</a></li><li><a href="https://github.com/Fingerzam">Juhana Laurinharju</a></li><li><a href="https://github.com/fangyi-zhou">Fangyi Zhou</a></li><li><a href="https://github.com/phi16">phi16</a></li><li><a href="https://github.com/jonaprieto">Jonathan Prieto</a></li><li><a href="https://github.com/kenichi-asai">Kenichi Asai</a></li><li><a href="https://github.com/livecodealex">Alexandru Brisan</a></li><li><a href="https://github.com/michel-steuwer">Michel Steuwer</a></li><li><a href="https://github.com/caryoscelus">caryoscelus</a></li><li><a href="https://github.com/lzmartinico">Lorenzo Martinico</a></li><li><a href="https://github.com/whxvd">Sebastian Miele</a></li><li><a href="https://github.com/odanoburu">bruno cuconato</a></li><li><a href="https://github.com/murilogiacometti">Murilo Giacometti Rocha</a></li><li><a href="https://github.com/gallais">G. Allais</a></li><li><a href="https://github.com/spwhitt">Spencer Whitt</a></li><li><a href="https://github.com/LightAndLight">Isaac Elliott</a></li><li><a href="https://github.com/iblech">Ingo Blechschmidt</a></li><li><a href="https://github.com/trajafri">Syed Turab Ali Jafri</a></li><li><a href="https://github.com/Teggy">Torsten Grust</a></li><li><a href="https://github.com/zenzike">Nicolas Wu</a></li><li><a href="https://github.com/k4rtik">Kartik Singhal</a></li><li><a href="https://github.com/philderbeast">Phil de Joux</a></li><li><a href="https://github.com/stepchowfun">Stephan Boyer</a></li><li><a href="https://github.com/zgrannan">Zack Grannan</a></li><li><a href="https://github.com/navaati">Léo Gillot-Lamure</a></li><li><a href="https://github.com/hugomg">Hugo Gualandi</a></li><li><a href="https://github.com/kwxm">Kenneth MacKenzie</a></li><li><a href="https://github.com/chikeabuah">Chike Abuah</a></li><li><a href="https://github.com/moleike">Alexandre Moreno</a></li><li><a href="https://github.com/laMudri">James Wood</a></li><li><a href="https://github.com/kranich">Stefan Kranich</a></li><li><a href="https://github.com/rodamber">Rodrigo Bernardo</a></li><li><a href="https://github.com/omelkonian">Orestis Melkonian</a></li><li><a href="https://github.com/dalpd">Deniz Alp</a></li><li><a href="https://github.com/potato4444">Nathaniel Carroll</a></li><li><a href="https://github.com/cyberglot">cyberglot</a></li><li>Vikraman Choudhury</li><li>Ben Darwin</li><li><a href="https://github.com/koo5">koo5</a></li><li>Anish Tondwalkar</li><li>Nils Anders Danielsson</li><li>Miëtek Bak</li><li>Gergő Érdi</li><li>Adam Sandberg Eriksson</li><li>David Janin</li><li>András Kovács</li><li>Ulf Norell</li><li>Liam O'Connor</li><li>N. Raghavendra</li><li>Roman Kireev</li><li>Amr Sabry</li><li>[Your name goes here]</li>
|
|
</ul>
|
|
<p>For support:</p>
|
|
<ul>
|
|
<li>EPSRC Programme Grant EP/K034413/1</li>
|
|
<li>NSF Grant No. 1814460</li>
|
|
<li>Foundation Sciences Mathematiques de Paris (FSMP)
|
|
Distinguised Professor Fellowship</li>
|
|
</ul>
|
|
|
|
</div>
|
|
|
|
<p style="text-align:center;">
|
|
|
|
<a alt="Previous chapter" href="/19.08/Untyped/">Prev</a>
|
|
|
|
|
|
•
|
|
|
|
|
|
|
|
|
|
<a alt="Next chapter" href="/19.08/Fonts/">Next</a>
|
|
|
|
</p>
|
|
|
|
|
|
</article>
|
|
|
|
</div>
|
|
</main><footer class="site-footer h-card">
|
|
<data class="u-url" href="/19.08/"></data>
|
|
|
|
<div class="wrapper">
|
|
|
|
<h2 class="footer-heading">Programming Language Foundations in Agda
|
|
</h2><div class="footer-col-wrapper">
|
|
<div class="footer-col footer-col-1">
|
|
<ul class="contact-list">
|
|
<li class="p-name">Philip Wadler</li>
|
|
<li><a class="u-email" href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a></li>
|
|
</ul>
|
|
</div>
|
|
|
|
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wadler"><svg class="svg-icon"><use xlink:href="/19.08/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wadler</span></a></li></ul>
|
|
</div>
|
|
|
|
<div class="footer-col footer-col-3"></div>
|
|
</div><div class="footer-col-wrapper">
|
|
<div class="footer-col footer-col-1">
|
|
<ul class="contact-list">
|
|
<li class="p-name">Wen Kokke</li>
|
|
<li><a class="u-email" href="mailto:wen.kokke@ed.ac.uk">wen.kokke@ed.ac.uk</a></li>
|
|
</ul>
|
|
</div>
|
|
|
|
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wenkokke"><svg class="svg-icon"><use xlink:href="/19.08/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wenkokke</span></a></li><li><a href="https://www.twitter.com/wenkokke"><svg class="svg-icon"><use xlink:href="/19.08/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">wenkokke</span></a></li></ul>
|
|
</div>
|
|
|
|
<div class="footer-col footer-col-3"></div>
|
|
</div><div class="footer-col-wrapper">
|
|
<div class="footer-col footer-col-1">
|
|
<ul class="contact-list">
|
|
<li class="p-name">Jeremy Siek</li>
|
|
<li><a class="u-email" href="mailto:jsiek@indiana.edu">jsiek@indiana.edu</a></li>
|
|
</ul>
|
|
</div>
|
|
|
|
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/jsiek"><svg class="svg-icon"><use xlink:href="/19.08/assets/minima-social-icons.svg#github"></use></svg> <span class="username">jsiek</span></a></li><li><a href="https://www.twitter.com/jeremysiek"><svg class="svg-icon"><use xlink:href="/19.08/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">jeremysiek</span></a></li></ul>
|
|
</div>
|
|
|
|
<div class="footer-col footer-col-3"></div>
|
|
</div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a>
|
|
</div>
|
|
</footer>
|
|
<!-- Import jQuery -->
|
|
<script type="text/javascript" src="/19.08/assets/jquery.js"></script>
|
|
|
|
<script type="text/javascript">
|
|
|
|
// Makes sandwhich menu works
|
|
$('.menu-icon').click(function(){
|
|
$('.trigger').toggle();
|
|
});
|
|
|
|
// Script which allows for foldable code blocks
|
|
$('div.foldable pre').each(function(){
|
|
var autoHeight = $(this).height();
|
|
var lineHeight = parseFloat($(this).css('line-height'));
|
|
|
|
var plus = $("<div></div>");
|
|
var horLine = $("<div></div>");
|
|
var verLine = $("<div></div>");
|
|
$(this).prepend(plus);
|
|
plus.css({
|
|
'position' : 'relative',
|
|
'float' : 'right',
|
|
'right' : '-' + (0.5 * lineHeight - 1.5) + 'px',
|
|
'width' : lineHeight,
|
|
'height' : lineHeight});
|
|
verLine.css({
|
|
'position' : 'relative',
|
|
'height' : lineHeight,
|
|
'width' : '3px',
|
|
'background-color' : '#C1E0FF'});
|
|
horLine.css({
|
|
'position' : 'relative',
|
|
'top' : '-' + (0.5 * lineHeight + 1.5) + 'px',
|
|
'left' : '-' + (0.5 * lineHeight - 1.5) + 'px',
|
|
'height' : '3px',
|
|
'width' : lineHeight,
|
|
'background-color' : '#C1E0FF'});
|
|
plus.append(verLine);
|
|
plus.append(horLine);
|
|
|
|
$(this).height(2.0 * lineHeight);
|
|
$(this).css('overflow','hidden');
|
|
|
|
$(this).click(function(){
|
|
if ($(this).height() == autoHeight) {
|
|
$(this).height(2.0 * lineHeight);
|
|
plus.show();
|
|
}
|
|
else {
|
|
$(this).height('auto');
|
|
plus.hide();
|
|
}
|
|
});
|
|
});
|
|
</script>
|
|
|
|
<!-- Import KaTeX -->
|
|
<script type="text/javascript" src="/19.08/assets/katex.js"></script>
|
|
|
|
<!-- Script which renders TeX using KaTeX -->
|
|
<script type="text/javascript">
|
|
$("script[type='math/tex']").replaceWith(
|
|
function(){
|
|
var tex = $(this).text();
|
|
return "<span class=\"inline-equation\">" +
|
|
katex.renderToString(tex) +
|
|
"</span>";
|
|
});
|
|
$("script[type='math/tex; mode=display']").replaceWith(
|
|
function(){
|
|
var tex = $(this).text().replace(/%.*?(\n|$)/g,"");
|
|
return "<div class=\"equation\">" +
|
|
katex.renderToString("\\displaystyle "+tex) +
|
|
"</div>";
|
|
});
|
|
</script>
|
|
</body>
|
|
|
|
</html>
|