Commit b3e8e356 authored by Nuria Brede's avatar Nuria Brede

Initial.

parent 0e36f495
@misc{idristutorial,
author = {Edwin Brady},
file = {/Users/edwin/Documents/Mendeley Desktop/Brady/Programming in Idris a tutorial/Brady - Programming in Idris a tutorial - 2012.pdf},
title = {Programming in {Idris} : a tutorial},
url = {http://idris-lang.org/tutorial},
year = {2013}
}
@book{idrisbook,
author = {Edwin Brady},
publisher = {Manning Publications Co.},
title = {Type-{D}riven {D}evelopment in {I}dris},
year = {2017}
}
@article{schoenfinkel1924,
author = {M. Sch{\"o}nfinkel},
journal = {Mathematische Annalen},
pages = {305--316},
title = {{\"U}ber die Bausteine der mathematischen Logik},
year = 1924
}
@misc{botta20162020,
author = {Nicola Botta},
howpublished = {\url{https://gitlab.pik-potsdam.de/botta/IdrisLibs}},
title = {{I}dris{L}ibs},
year = {2016--2018}
}
@Article{esd-9-525-2018,
AUTHOR = {Botta, N. and Jansson, P. and Ionescu, C.},
TITLE = {The impact of uncertainty on optimal emission policies},
JOURNAL = {Earth System Dynamics},
VOLUME = {9},
YEAR = {2018},
NUMBER = {2},
PAGES = {525--542},
URL = {https://www.earth-syst-dynam.net/9/525/2018/},
DOI = {10.5194/esd-9-525-2018}
}
@inproceedings{ionescujansson:LIPIcs:2013:3899,
address = {Dagstuhl, Germany},
annote = {Keywords: dependently-typed programming, domain-specific languages, climate impact research, formalization},
author = {Cezar Ionescu and Patrik Jansson},
booktitle = {Proc. TYPES 2011},
commenteditor = {Nils Anders Danielsson and Bengt Nordstr{\"o}m},
commentisbn = {978-3-939897-49-1},
commentissn = {1868-8969},
commenturl = {http://drops.dagstuhl.de/opus/volltexte/2013/3899},
doi = {10.4230/LIPIcs.TYPES.2011.41},
longbooktitle = {18th International Workshop on Types for Proofs and Programs (TYPES 2011)},
pages = {41--54},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
title = {Testing versus proving in climate impact research},
volume = 19,
year = 2013
}
@book{bellman1957,
author = {Richard Bellman},
publisher = {Princeton University Press},
title = {Dynamic Programming},
year = {1957}
}
@article{2017_Botta_Jansson_Ionescu,
author = {Nicola Botta and Patrik Jansson and Cezar Ionescu},
journal = {J. Funct. Program.},
number = {27, e23},
title = {Contributions to a computational theory of policy advice and avoidability},
year = 2017
}
@article{2014_Botta_et_al,
author = {Nicola Botta and Patrik Jansson and Cezar Ionescu and David R. Christiansen and Edwin Brady},
bibsource = {dblp computer science bibliography, http://dblp.org},
biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/BottaJICB16},
doi = {10.23638/LMCS-13(1:7)2017},
journal = {Logical Methods in Computer Science},
number = 1,
timestamp = {Wed, 03 May 2017 14:47:56 +0200},
title = {Sequential decision problems, dependent types and generic solutions},
volume = 13,
year = 2017
}
@phdthesis{ionescu2009,
author = {Cezar Ionescu},
school = {Freie Universit{\"a}t Berlin},
title = {Vulnerability Modelling and Monadic Dynamical Systems},
url = {https://d-nb.info/1023491036/34},
year = 2009
}
@incollection{Ross2008-ROSGT,
author = {Don Ross},
booktitle = {Stanford Encyclopedia of Philosophy},
title = {Game Theory},
year = {2008}
}
@incollection{sep-decision-causal,
author = {Paul Weirich},
booktitle = {The Stanford Encyclopedia of Philosophy},
edition = {Winter 2016},
editor = {Edward N. Zalta},
howpublished = {\url{https://plato.stanford.edu/archives/win2016/entries/decision-causal/}},
publisher = {Metaphysics Research Lab, Stanford University},
title = {Causal Decision Theory},
year = {2016}
}
@inproceedings{DBLP:conf/lics/Moggi89,
author = {Eugenio Moggi},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/bib/conf/lics/Moggi89},
booktitle = {Proceedings of the Fourth Annual Symposium on Logic in Computer Science {(LICS} '89), Pacific Grove, California, USA, June 5-8, 1989},
crossref = {DBLP:conf/lics/1989},
doi = {10.1109/LICS.1989.39155},
pages = {14--23},
timestamp = {Wed, 16 Oct 2019 14:14:54 +0200},
title = {Computational Lambda-Calculus and Monads},
url = {https://doi.org/10.1109/LICS.1989.39155},
year = {1989}
}
@article{DBLP:journals/cacm/Wadler15,
author = {Philip Wadler},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/bib/journals/cacm/Wadler15},
doi = {10.1145/2699407},
journal = {Commun. {ACM}},
number = {12},
pages = {75--84},
timestamp = {Wed, 14 Nov 2018 10:22:36 +0100},
title = {Propositions as types},
url = {https://doi.org/10.1145/2699407},
volume = {58},
year = {2015}
}
@inproceedings{DBLP:conf/fpca/Wadler89,
author = {Philip Wadler},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/bib/conf/fpca/Wadler89},
booktitle = {Proceedings of the fourth international conference on Functional programming languages and computer architecture, {FPCA} 1989, London, UK, September 11-13, 1989},
crossref = {DBLP:conf/fpca/1989},
doi = {10.1145/99370.99404},
pages = {347--359},
timestamp = {Wed, 14 Nov 2018 10:57:36 +0100},
title = {Theorems for Free!},
url = {https://doi.org/10.1145/99370.99404},
year = {1989}
}
@inproceedings{DBLP:conf/nato/Wadler92,
author = {Philip Wadler},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/bib/conf/nato/Wadler92},
booktitle = {Program Design Calculi, Proceedings of the {NATO} Advanced Study Institute on Program Design Calculi, Marktoberdorf, Germany, July 28 - August 9, 1992},
crossref = {DBLP:conf/nato/1992pdc},
doi = {10.1007/978-3-662-02880-3\_8},
pages = {233--264},
timestamp = {Sun, 14 May 2017 18:58:39 +0200},
title = {Monads for functional programming},
url = {https://doi.org/10.1007/978-3-662-02880-3\_8},
year = {1992}
}
@book{DBLP:books/daglib/0096998,
author = {Richard S. Bird and Oege de Moor},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/bib/books/daglib/0096998},
isbn = {978-0-13-507245-5},
publisher = {Prentice Hall},
series = {Prentice Hall International series in computer science},
timestamp = {Thu, 03 Feb 2011 12:08:27 +0100},
title = {Algebra of programming},
year = {1997}
}
@book{DBLP:books/daglib/0073499,
author = {Carroll Morgan},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/bib/books/daglib/0073499},
isbn = {978-0-13-123274-7},
publisher = {Prentice Hall},
series = {Prentice Hall International series in computer science},
timestamp = {Thu, 22 Feb 2018 18:20:56 +0100},
title = {Programming from specifications, 2nd Edition},
year = {1994}
}
@article{Ionescu_2016,
author = {Cezar Ionescu and Patrik Jansson},
doi = {10.4204/eptcs.230.1},
issn = {2075-2180},
journal = {Electronic Proceedings in Theoretical Computer Science},
month = {Nov},
pages = {1--15},
publisher = {Open Publishing Association},
title = {Domain-Specific Languages of Mathematics: Presenting Mathematical Analysis Using Functional Programming},
url = {http://dx.doi.org/10.4204/EPTCS.230.1},
volume = {230},
year = {2016}
}
@misc{DSLsofMathProject,
author = {Patrik Jansson and Cezar Ionescu},
title = {Domain Specific Languages of Mathematics (DSLsofMath)},
url = {https://www.chalmers.se/en/projects/Pages/Domain-Specific-Languages-of-Mathematics-QDSLsofMathQ.aspx},
year = {2014-2020}
}
@book{Kuznetsov:1998:EAB:289919,
address = {Berlin, Heidelberg},
author = {Yuri A. Kuznetsov},
isbn = {0-387-98382-1},
publisher = {Springer-Verlag},
title = {Elements of Applied Bifurcation Theory (2Nd Ed.)},
year = {1998}
}
@book{DBLP:books/daglib/0067018,
author = {Carroll Morgan},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/bib/books/daglib/0067018},
isbn = {978-0-13-726233-5},
publisher = {Prentice Hall},
series = {Prentice Hall International Series in computer science},
timestamp = {Thu, 22 Feb 2018 18:20:56 +0100},
title = {Programming from specifications},
year = {1990}
}
@article{Reynolds1998,
day = {01},
doi = {10.1023/A:1010027404223},
issn = {1573-0557},
journal = {Higher-Order and Symbolic Computation},
month = {Dec},
number = {4},
pages = {363--397},
title = {Definitional Interpreters for Higher-Order Programming Languages},
url = {https://doi.org/10.1023/A:1010027404223},
volume = {11},
year = {1998}
}
@inbook{QuineVanHeijenoort,
author = {W. Orman van Quine},
booktitle = {From Frege to G{\"o}del: A Source Book in Mathematical Logic, 1879-1931},
editor = {J. {Van Heijenoort}},
isbn = {9780674324497},
lccn = {67010905},
pages = {355--357},
publisher = {Harvard University Press},
series = {Source books in the history of the sciences},
title = {Introduction to Moses Sch{\"o}nfinkel's "Bausteine der mathematischen Logik"},
url = {https://books.google.be/books?id=v4tBTBlU05sC},
year = {1967}
}
@proceedings{DBLP:conf/lics/1989,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/bib/conf/lics/1989},
isbn = {0-8186-1954-6},
publisher = {{IEEE} Computer Society},
timestamp = {Wed, 16 Oct 2019 14:14:54 +0200},
title = {Proceedings of the Fourth Annual Symposium on Logic in Computer Science {(LICS} '89), Pacific Grove, California, USA, June 5-8, 1989},
url = {https://ieeexplore.ieee.org/xpl/conhome/249/proceeding},
year = {1989}
}
@proceedings{DBLP:conf/fpca/1989,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/bib/conf/fpca/1989},
doi = {10.1145/99370},
editor = {Joseph E. Stoy},
isbn = {0-201-51389-7},
publisher = {{ACM}},
timestamp = {Tue, 06 Nov 2018 11:07:48 +0100},
title = {Proceedings of the fourth international conference on Functional programming languages and computer architecture, {FPCA} 1989, London, UK, September 11-13, 1989},
url = {https://doi.org/10.1145/99370},
year = {1989}
}
@proceedings{DBLP:conf/nato/1992pdc,
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/bib/conf/nato/1992pdc},
doi = {10.1007/978-3-662-02880-3},
editor = {Manfred Broy},
isbn = {978-3-642-08164-4},
publisher = {Springer},
series = {{NATO} {ASI} Series},
timestamp = {Sun, 14 May 2017 18:55:41 +0200},
title = {Program Design Calculi, Proceedings of the {NATO} Advanced Study Institute on Program Design Calculi, Marktoberdorf, Germany, July 28 - August 9, 1992},
url = {https://doi.org/10.1007/978-3-662-02880-3},
volume = {118},
year = {1993}
}
@book{curryFeys,
title={Combinatory Logic},
author={Curry, H.B. and Feys, R.},
number={v. 1},
lccn={a59001593},
series={Combinatory Logic},
url={https://books.google.be/books?id=fEnuAAAAMAAJ},
year={1958},
publisher={North-Holland Publishing Company}
}
\ No newline at end of file
---
title: Aims and plans
author: Nicola Botta, Nuria Brede, Potsdam Institute for Climate Impact Research
date: 2019-10-28
geometry: margin=2cm
fontsize: 10pt
---
# Objectives of the course
* Learn to specify and solve decision problems in climate research
* Understand the basics of decision making under uncertainty
* Understand optimal policies and accountable decision making
# Structure
* A series of basic lectures + exercises to achieve the objectives of
the course (L1 - L10)
* Extra lectures (L1E1, L2E1, L3E1, ...) to deepen, point out
connections, ... have more fun!
# Tentative course plan
* L1: Decision problems in climate research
- L1E1: What are formal methods?
("Modelling vs. formalization", Example from DSL of math)
* L2: Mathematical specifications
- L2E1: Newcomb's dilemma
* L3: A crash-course in functional programming
- L3E1: Install and use Idris and emacs' Idris mode
- L3E2: Folds and initial algebras
* L4: Dependent types and machine checkable specifications
- L4E1: FOL and propositions-as-types
* L5: Time discrete dynamical systems
- L5E1: Functors and monads from a CT angle
* L6: Time discrete monadic dynamical systems
* L7: Deterministic sequential decision problems, naive theory
* L8: Viability and reachability
* L9: Generic optimal extensions, viability and reachability tests
* L10: Extending the theory to monadic SDPs
* L11: Specifying an emission problem
# Tentative time plan
* Day 1: Make a time plan, L1, L2 and perhaps L1E1?
* Day 2: L1 and L2 exercises, install and use Idris, L2E1?
* Day 3: L3, L3 exercises and L3E2?
* Day 4: L4, L4 exercises and L4E1?
* Day 5: L5
* Day 6: L5E1, L6
* Day 7: L7, L8
* Day 8: L9
* Day 9: L10
* Day 10: L11
% -*-Latex-*-
\documentclass{article}
\input{setup.tex}
%include lhs.fmt
\input{macros.TeX}
\begin{document}
%include Lecture10.lidr
\bibliographystyle{plain}
\bibliography{references}
\end{document}
% -*-Latex-*-
\documentclass{article}
\input{setup.tex}
%include lhs.fmt
%format one = 1
%format `NonNegDouble.Predicates.LTE` = "\leq"
%format SequentialDecisionProblems.CoreTheory.State = X
%format SequentialDecisionProblems.CoreTheory.Ctrl = Y
%format SequentialDecisionProblems.CoreTheory.next = next
%format SequentialDecisionProblems.CoreTheory.reward = reward
%format SequentialDecisionProblems.CoreTheory.Val = Val
%format SequentialDecisionProblems.CoreTheory.plus = plus
%format SequentialDecisionProblems.CoreTheory.zero = zero
%format SequentialDecisionProblems.CoreTheory.LTE = "(\leq)"
%format SequentialDecisionProblems.FullTheory.reflexiveLTE = reflexiveLTE
%format SequentialDecisionProblems.FullTheory.transitiveLTE = transitiveLTE
%format SequentialDecisionProblems.FullTheory.monotonePlusLTE = monotonePlusLTE
%format SequentialDecisionProblems.CoreTheoryOptDefaults.totalPreorderLTE = totalPreorderLTE
%format SequentialDecisionProblems.CoreTheory.meas = meas
%format SequentialDecisionProblems.FullTheory.measMon = measMon
%format SequentialDecisionProblems.CoreTheory.Viable = Viable
%format SequentialDecisionProblems.CoreTheory.Reachable = Reachable
%format SequentialDecisionProblems.CoreTheory.viableSpec1 = viableSpec1
%format SequentialDecisionProblems.CoreTheory.NotEmpty = NotEmpty
%format SequentialDecisionProblems.CoreTheory.All = All
%format SequentialDecisionProblems.Utils.finiteViable = finiteViable
%format SequentialDecisionProblems.Utils.decidableViable = decidableViable
%format SequentialDecisionProblems.CoreTheory.reachableSpec1 = reachableSpec1
%format SequentialDecisionProblems.TabBackwardsInduction.decidableReachable = decidableReachable
%format SequentialDecisionProblems.Utils.finiteCtrl = finiteCtrl
%format SequentialDecisionProblems.TabBackwardsInduction.finiteState = finiteState
%format SequentialDecisionProblems.Utils.showState = showState
%format SequentialDecisionProblems.Utils.showCtrl = showCtrl
\input{macros.TeX}
\begin{document}
%include Lecture11.lidr
\pagebreak
\bibliographystyle{plain}
\bibliography{references}
\end{document}
% -*-Latex-*-
\documentclass{article}
\input{setup.tex}
%include lhs.fmt
\input{macros.TeX}
\begin{document}
%include Lecture2.lidr
\bibliographystyle{plain}
\bibliography{references}
\end{document}
% -*-Latex-*-
\documentclass{article}
\input{setup.tex}
%include lhs.fmt
\input{macros.TeX}
\begin{document}
%include Lecture3.lidr
\bibliographystyle{plain}
\bibliography{references}
\end{document}
% -*-Latex-*-
\documentclass{article}
\input{setup.tex}
%include lhs.fmt
\input{macros.TeX}