90 lines
3.6 KiB
BibTeX
90 lines
3.6 KiB
BibTeX
@article{NBE2016,
|
||
title={Normalisation by Evaluation for Dependent Types},
|
||
author={Thorsten Altenkirch and Ambrus Kaposi},
|
||
booktitle={International Conference on Formal Structures for Computation and Deduction},
|
||
year={2016}
|
||
}
|
||
@phdthesis{AltenkirschThesis1993,
|
||
title={Constructions, inductive types and strong normalization},
|
||
author={Thorsten Altenkirch},
|
||
booktitle={CST},
|
||
year={1993}
|
||
}
|
||
@unpublished{TaoOfTypes,
|
||
title={The Tao of Types},
|
||
author={Thorsten Altenkirsch}
|
||
}
|
||
@inproceedings{folSogatKaposi2023,
|
||
title={Why is equality interesting?},
|
||
author={Ambrus Kaposi},
|
||
url={https://akaposi.github.io/pres_wld.pdf}}
|
||
|
||
@phdthesis{UemuraThesis2021,
|
||
title = {Abstract and concrete type theories},
|
||
isbn = {9789464213768},
|
||
url = {https://dare.uva.nl/search?identifier=41ff0b60-64d4-4003-8182-c244a9afab3b},
|
||
language = {en},
|
||
urldate = {2023-08-04},
|
||
publisher = {AmsterdamInstitute for Logic, Language and Computation},
|
||
author = {Uemura, T.},
|
||
year = {2021},
|
||
}
|
||
|
||
@article{logicalFramework1993,
|
||
author = {Harper, Robert and Honsell, Furio and Plotkin, Gordon},
|
||
title = {A Framework for Defining Logics},
|
||
year = {1993},
|
||
issue_date = {Jan. 1993},
|
||
publisher = {Association for Computing Machinery},
|
||
address = {New York, NY, USA},
|
||
volume = {40},
|
||
number = {1},
|
||
issn = {0004-5411},
|
||
url = {https://doi.org/10.1145/138027.138060},
|
||
doi = {10.1145/138027.138060},
|
||
abstract = {The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed λ-calculus with dependent types. Syntax is treated in a style similar to, but more general than, Martin-Lo¨f's system of arities. The treatment of rules and proofs focuses on his notion of a judgment. Logics are represented in LF via a new principle, the judgments as types principle, whereby each judgment is identified with the type of its proofs. This allows for a smooth treatment of discharge and variable occurence conditions and leads to a uniform treatment of rules and proofs whereby rules are viewed as proofs of higher-order judgments and proof checking is reduced to type checking. The practical benefit of our treatment of formal systems is that logic-independent tools, such as proof editors and proof checkers, can be constructed.},
|
||
journal = {J. ACM},
|
||
month = {jan},
|
||
pages = {143–184},
|
||
numpages = {42},
|
||
keywords = {formal systems, interactive theorem proving, proof checking, typed lambda calculus}
|
||
}
|
||
|
||
@article{hoffmann1999,
|
||
author = {Hofmann, Martin},
|
||
title = {Semantical Analysis of Higher-Order Abstract Syntax},
|
||
year = {1999},
|
||
isbn = {0769501583},
|
||
publisher = {IEEE Computer Society},
|
||
address = {USA},
|
||
abstract = {A functor category semantics for higher-order abstract syntax is proposed with the following aims: relating higher-order and first order syntax, justifying induction principles, suggesting new logical principles to reason about higher-order syntax},
|
||
booktitle = {Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science},
|
||
pages = {204},
|
||
series = {LICS '99}
|
||
}
|
||
|
||
@article{fioreMahmoud2013secondorder,
|
||
title={Second-Order Algebraic Theories},
|
||
author={Marcelo Fiore and Ola Mahmoud},
|
||
year={2013},
|
||
eprint={1308.5409},
|
||
archivePrefix={arXiv},
|
||
primaryClass={cs.LO}
|
||
}
|
||
@article{RedFreeNorm1995,
|
||
doi = {10.1007/3-540-60164-3_27},
|
||
url = {https://doi.org/10.1007\3-540-60164-3_27},
|
||
year = 1995,
|
||
publisher = {Springer Berlin Heidelberg},
|
||
pages = {182--199},
|
||
author = {Thorsten Altenkirch and Martin Hofmann and Thomas Streicher},
|
||
title = {Categorical reconstruction of a reduction free normalization proof},
|
||
booktitle = {Category Theory and Computer Science}
|
||
}
|
||
|
||
|
||
|
||
|
||
|
||
|