TalksA selection of talks that I have given:- Some tricks for making Agda code faster
Talk/discussion at
Agda
Implementors' Meeting XXXII, 2020-06-01.
["slides"] - Logical properties of a modality for erasure
Talk given at meeting
#79
of IFIP
WG2.1, Otterlo, 2020-01-06.
[pdf] - Some theory about nothing
Talk given at the
Logic and Types division meeting,
Aspenäs, 2019-09-21.
[pdf] - Up-to Techniques using Sized Types
Talk given at POPL 2018,
Los Angeles, 2018-01-11.
[pdf, video] - Up-to Techniques Using Sized Types
Talk given at the Joint Stockholm–Göteborg type theory
seminar, Göteborg, 2017-10-25.
[pdf] - Up-to Techniques Using Sized Types
Talk given at meeting
#76
of IFIP
WG2.1, Lesbos, 2017-10-17.
[pdf] - Higher and/or dependent lenses
Agda Implementors' Meeting XXII,
Leuven, 2015–09–16.
[pdf, accompanying code] - Isomorphism is equality
Talk given at meeting
#73
of IFIP
WG2.1, Lökeberg, 2015-08-25.
[pdf] - Nested induction and coinduction
Docent lecture, 2014-06-13.
(Slightly edited.) [abstract, pdf] - Operational Semantics Using the Partiality Monad
Talk given at
Shonan Meeting 026: Coinduction for computation structures
and programming languages, Shonan Village Center,
2013-10-08.
[abstract, pdf] - Correct-by-Construction Pretty-Printing
Talk given at
DTP 2013,
Boston, MA, 2013-09-25.
[pdf] - Correct-by-Construction Pretty-Printing
Talk given at meeting
#70
of IFIP
WG2.1, Schloss Reisensburg, 2013-07-04.
(Slightly edited.) [abstract, pdf] - Operational Semantics Using the Partiality Monad
Talk given at
ICFP 2012,
København, 2012-09-10.
[pdf, video] - Bag Equivalence via a Proof-Relevant Membership Relation
Talk given at
ITP 2012,
Princeton, 2012-08-14.
[pdf] - Calculating Bag Equalities
Talk given at meeting
#68
of IFIP
WG2.1, Rome, 2012-02-06.
(Slightly edited.) [abstract, pdf] - Total Parser Combinators
Talk given at
ICFP 2010,
Baltimore, 2010-09-29.
(Slightly edited.) [pdf, video] - Total Parser Combinators Using Mixed Induction and Coinduction
Talk given at meeting
#66
of IFIP
WG2.1, Atlantic City, 2010-09-20.
[abstract, pdf] - Beating the Productivity Checker Using Embedded Languages
Talk given at
PAR 2010,
Edinburgh, 2010-07-15.
[pdf] - Operational Semantics Using the Partiality Monad
Talk given at
DTP 2010,
Edinburgh, 2010-07-09.
[abstract, pdf, accompanying code] - Subtyping, Declaratively
An Exercise in Mixed Induction and Coinduction Talk given at
MPC 2010,
Lac-Beauport, Québec, 2010-06-23.
[pdf] - Operational Semantics Using the Partiality Monad
Agda Implementors' Meeting XI,
Awaji Yumebutai, 2010-03-24.
(Slightly edited.) [abstract, pdf, accompanying code] - Total Parser Combinators
MGS Christmas Seminars 2009,
Sheffield, 2009-12-15.
For more information, see
Total Parser Combinators.
[abstract, pdf] - Mixing Induction and Coinduction
TYPES 2009,
Aussois, 2009-05-15.
For more information, see
Total Parser Combinators and
Subtyping, Declaratively.
[abstract, pdf] - Structurally Recursive Descent Parsing
Logic and Semantics Seminar, Cambridge, 2009-03-20. [abstract, pdf] - An ad-hoc and monolithic method for ensuring that corecursive definitions are productive
Agda Intensive Meeting 9,
Sendai, 2008-11-27.
(Slightly edited.) For more information, see
Beating the Productivity
Checker Using Embedded Languages.
[abstract, pdf, pdf (n-up)] - Parsing Mixfix Operators
IFL 2008,
Hatfield, 2008-09-10.
[pdf, pdf (n-up)] - Improved handling of mixfix operators: Design and implementation
Agda Implementors' Meeting 8,
Göteborg, 2008-05-29.
[pdf, pdf (n-up)] - Structurally Recursive Descent Parsing
Dependently Typed Programming 2008,
Nottingham, 2008-02-18.
[abstract, pdf, pdf (n-up)] - Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures
POPL 2008,
San Francisco, 2008-01-10.
(Slightly edited.) [pdf, pdf (n-up)] - A Well-typed Interpreter for a Dependently Typed Language
Fun in the Afternoon, Nottingham, 2007-02-21. [abstract, pdf, pdf (n-up)] - A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family
Proglog meeting, 2007-01-31. Slides slightly edited. [abstract, pdf, pdf (n-up)] - Fast and Loose Reasoning is Morally Correct
POPL 2006, 2006-01-12. [pdf] - Cover Summary
Talk given for the Programatica group, 2005-03-18. [pdf] - Chasing Bottoms, A Case Study in Program Verification in the Presence of Partial and Infinite Values
MPC 2004, the Seventh International Conference on Mathematics of Program Construction, Stirling, UK, July 2004. [pdf, ps.gz (n-up)] - Factoring is in BQP
Algorithms Research Seminar, 2003-05-12. [abstract] - Introduction to Quantum Computation
Algorithms Research Seminar, 2003-04-28. [abstract, pdf] - Matroids from Modules
MFCSIT2002, the Second Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, National University of Ireland, Galway, July 2002. [pdf, ps.gz] Nils Anders Danielsson Last updated Fri Aug 25 13:09:47 UTC 2023. |