Article Open Access
- Author:
- Thiago Felicissimo https://ror.org/03xjwb503Université Paris-Saclay, INRIA, LMF, ENS Paris-Saclay, Gif-sur-Yvette, France
https://ror.org/03xjwb503Université Paris-Saclay, INRIA, LMF, ENS Paris-Saclay, Gif-sur-Yvette, France
View Profile
Programming Languages and Systems: 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part IApr 2024Pages 171–175https://doi.org/10.1007/978-3-031-57262-3_7
Published:06 April 2024Publication History
- 0citation
- 0
- Downloads
Metrics
Total Citations0Total Downloads0Last 12 Months0
Last 6 weeks0
- Get Citation Alerts
New Citation Alert added!
This alert has been successfully added and will be sent to:
You will be notified whenever a record that you have chosen has been cited.
To manage your alert preferences, click on the button below.
Manage my Alerts
New Citation Alert!
Please log in to your account
See AlsoMeaningful Consensus or Delaying Disagreements? UNCITRAL Working Group III and the Advisory Centre on International Investment Dispute Resolution - Kluwer Arbitration BlogFrom Evasion to Enforcement: How the English Commercial Court Recaptured NIOC’s Undervalued Property Transfer to Enforce an Arbitral Award - Kluwer Arbitration BlogThe Enforceability of DIFC-LCIA Arbitration Clauses in Light of Decree No. 34/2021: A View from Outside the UAE - Kluwer Arbitration BlogTHE UNIVERSE OF THE DIRECTIONS - [PDF Document] - Publisher Site
Programming Languages and Systems: 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part I
Artifact report: Generic bidirectional typing for dependent type theories
Pages 171–175
PreviousChapterNextChapter
Abstract
We report on the implementation of a generic bidirectional algorithm for dependent type theories, following the proposal of the paper "Generic bidirectional typing for dependent type theories".
References
- 1.Abel, A.: Normalization by evaluation: Dependent types and impredicativity. Habilitation. Ludwig-Maximilians-Universität München (2013)Google Scholar
- 2.Assaf, A., Burel, G., Cauderlier, R., Delahaye, D., Dowek, G., Dubois, C., Gilbert, F., Halmagrand, P., Hermant, O., Saillard, R.: Dedukti: a logical framework based on the -calculus modulo theory (2016), unpublishedGoogle Scholar
- 3.Blanqui, F., Dowek, G., Grienenberger, É., Hondet, G., Thiré, F.: Some axioms for mathematics. In: Kobayashi, N. (ed.) 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference). LIPIcs, vol.195, pp. 20:1–20:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). DOI: https://doi.org/10.4230/LIPIcs.FSCD.2021.20, https://doi.org/10.4230/LIPIcs.FSCD.2021.20Google ScholarCross Ref
- 4.Coquand, T.: An algorithm for type-checking dependent types. Science of Computer Programming 26(1-3), 167–177 (1996)Google Scholar
- 5.Felicissimo, T.: Generic bidirectional typing for dependent type theories (2023)Google Scholar
- 6.Felicissimo, T.: BiTTs (Jan 2024). DOI: https://doi.org/10.5281/zenodo.10500598, https://doi.org/10.5281/zenodo.10500598Google ScholarCross Ref
- 7.Gratzer, D., Sterling, J., Birkedal, L.: Implementing a modal dependent type theory. Proceedings of the ACM on Programming Languages 3(ICFP), 1–29 (2019)Google Scholar
- 8.Kovács, A.: elaboration-zoo (2023), https://github.com/AndrasKovacs/elaboration-zooGoogle Scholar
Cited By
View all
Recommendations
- Generic bidirectional typing for dependent type theories
Programming Languages and Systems
Abstract
Bidirectional typing is a discipline in which the typing judgment is decomposed explicitly into inference and checking modes, allowing to control the flow of type information in typing rules and to specify algorithmically how they should be used. ...
Read More
- Bidirectional Typing
Bidirectional typing combines two modes of typing: type checking, which checks that a program satisfies a known type, and type synthesis, which determines a type from the program. Using checking enables bidirectional typing to support features for which ...
Read More
- Label dependent lambda calculus and gradual typing
Dependently-typed programming languages are gaining importance, because they can guarantee a wide range of properties at compile time. Their use in practice is often hampered because programmers have to provide very precise types. Gradual typing is a ...
Read More
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in
Full Access
Get this Publication
- Information
- Contributors
Published in
Programming Languages and Systems: 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6–11, 2024, Proceedings, Part I
Apr 2024
350 pages
ISBN:978-3-031-57261-6
DOI:10.1007/978-3-031-57262-3
- Editor:
- Stephanie Weirich
https://ror.org/00b30xv10University of Pennsylvania, Philadelphia, PA, USA
© The Author(s) 2024
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
Sponsors
In-Cooperation
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
- Published: 6 April 2024
Qualifiers
- Article
Conference
Funding Sources
Other Metrics
View Article Metrics
- Bibliometrics
- Citations0
Article Metrics
- View Citations
Total Citations
Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Other Metrics
View Author Metrics
Cited By
This publication has not been cited yet
Digital Edition
View this article in digital edition.
View Digital Edition
- Figures
- Other
Close Figure Viewer
Browse AllReturn
Caption
View Table of Contents
Export Citations
Your Search Results Download Request
We are preparing your search results for download ...
We will inform you here when the file is ready.
Download now!
Your Search Results Download Request
Your file of search results citations is now ready.
Download now!
Your Search Results Download Request
Your search export query has expired. Please try again.
