%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% String Definitions %%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Publishing houses
% %%%%%%%%%%%%%%%%%
@STRING{ap = "Academic Press" }
@STRING{springer = {Springer-Verlag} }
@STRING{lncs = "Lecture Notes in Computer Science" }
@STRING{lnm = "Lecture Notes in Mathematics" }
@STRING{gtm = "Graduate Texts in Mathematics" }
@STRING{lfcs = "Laboratory for Foundations of Computer Science,
University of Edinburgh" }
@STRING{mp = "MIT Press" }
@STRING{mitpress = mp }
%
% Journals and magazines
% %%%%%%%%%%%%%%%%%%%%%%
@STRING{toplas = "ACM Transactions on Programming Languages and Systems" }
@STRING{jlp = {Journal of Logic Programming} }
@STRING{cacm = "Communications of the {ACM}" }
@STRING{jacm = "Journal of the {ACM}" }
@STRING{tcs = "Theoretical Computer Science" }
@STRING{jsl = "Journal of Symbolic Logic" }
@STRING{siamjc = "SIAM Journal on Computing" }
@STRING{mscs = "Mathematical Structures in Computer Science" }
@STRING{proc = "Proceedings of the" }
@STRING{ic = "Information and Computation" }
@STRING{iandcomp = {Information and Computation} }
@string{ifip = "International Federation for Information Processing World Computer Congress (IFIP)"}
@STRING{jfp = "Journal of Functional Programming" }
@STRING{lmcs = "Logical Methods in Computer Science" }
@string{hosc = "Higher-Order and Symbolic Computation"}
@STRING{cup = "Cambridge University Press" }
@STRING{mcgh = "McGraw-Hill" }
@STRING{nh = "North Holland" }
@STRING{sv = "Springer-Verlag" }
@STRING{aw = "Addison-Wesley" }
@STRING{ph = "Prentice Hall" }
@STRING{signot = "SIGPLAN Notices"}
@STRING{taoop = "Carl A. Gunter and John C. Mitchell, editors, {\em
Theoretical Aspects of Object-Oriented Programming:
Types, Semantics, and Language Design}, MIT Press, 1994" }
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Conferences %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@STRING{popl = "{ACM} {S}ymposium on {P}rinciples of {P}rogramming
{L}anguages ({POPL})" }
@STRING{popl73 = popl # ", Boston, Massachusetts" }
@STRING{popl75 = popl # ", Palo Alto, California" }
@STRING{popl76 = popl # ", {A}tlanta, {G}eorgia" }
@STRING{popl77 = popl # ", Los Angeles, California" }
@STRING{popl78 = popl # ", Tucson, Arizona" }
@STRING{popl79 = popl # ", San Antonio, Texas" }
@STRING{popl80 = popl # ", Las Vegas, Nevada" }
@STRING{popl81 = popl # ", Williamsburg, Virginia" }
@STRING{popl82 = popl # ", Albuquerque, New Mexico" }
@STRING{popl83 = popl # ", Austin, Texas" }
@STRING{popl84 = popl # ", Salt Lake City, Utah" }
@STRING{popl85 = popl # ", New Orleans, Louisiana" }
@STRING{popl86 = popl # ", St.\ Petersburg Beach, Florida" }
@STRING{popl87 = popl # ", Munich, Germany" }
@STRING{popl88 = popl # ", San Diego, California" }
@STRING{popl89 = popl # ", Austin, Texas" }
@STRING{popl90 = popl # ", {S}an {F}rancisco, {C}alifornia" }
@STRING{popl91 = popl # ", Orlando, Florida" }
@STRING{popl92 = popl # ", Albuquerque, New Mexico" }
@STRING{popl93 = popl # ", Charleston, South Carolina" }
@STRING{popl94 = popl # ", {P}ortland, {O}regon" }
@STRING{popl95 = popl # ", San Francisco, California" }
@STRING{popl96 = popl # ", St.~Petersburg Beach, Florida" }
@STRING{popl97 = popl # ", Paris, France" }
@STRING{popl98 = popl # ", San Diego, California" }
@STRING{popl99 = popl # ", San Antonio, Texas" }
@STRING{popl00 = popl # ", Boston, Massachusetts" }
@STRING{popl01 = popl # ", London, England" }
@STRING{popl02 = popl # ", Portland, Oregon" }
@STRING{popl03 = popl # ", New Orleans, Louisiana" }
@STRING{popl04 = popl # ", Venice, Italy" }
@STRING{popl05 = popl # ", Long Beach, California" }
@STRING{popl06 = popl # ", Charleston, South Carolina" }
@STRING{popl07 = popl # ", Nice, France" }
@STRING{popl08 = popl # ", San Francisco, California" }
@STRING{popl09 = popl # ", Savannah, Georgia" }
@STRING{popl10 = popl # ", Madrid, Spain" }
@STRING{popl11 = popl # ", Austin, Texas" }
@STRING{popl12 = popl # ", Philadelphia, Pennsylvania" }
@STRING{popl13 = popl # ", Rome, Italy" }
@STRING{popl14 = popl # ", San Diego, California" }
@STRING{popl15 = popl # ", Mumbai, India" }
@STRING{popl16 = popl # ", St. Petersburg, Florida" }
@STRING{popl19 = popl # ", Cascais, Portugal" }
% ----
@STRING{icfp = "{I}nternational {C}onference on {F}unctional {P}rogramming
({ICFP})" }
@STRING{icfp96 = icfp # ", Philadelphia, Pennsylvania" }
@STRING{icfp97 = icfp # ", Amsterdam, The Netherlands" }
@STRING{icfp98 = icfp # ", Baltimore, Maryland, USA" }
@STRING{icfp99 = icfp # ", Paris, France" }
@STRING{icfp00 = icfp # ", Montreal, Canada" }
@STRING{icfp01 = icfp # ", Firenze, Italy" }
@STRING{icfp02 = icfp # ", Pittsburgh, Pennsylvania" }
@STRING{icfp03 = icfp # ", Uppsala, Sweden" }
@STRING{icfp04 = icfp # ", Snowbird, Utah" }
@STRING{icfp05 = icfp # ", Tallinn, Estonia" }
@STRING{icfp06 = icfp # ", Portand, Oregon" }
@STRING{icfp07 = icfp # ", Freiburg, Germany" }
@STRING{icfp08 = icfp # ", Victoria, British Columbia, Canada" }
@STRING{icfp09 = icfp # ", Edinburgh, Scotland" }
@STRING{icfp10 = icfp # ", Baltimore, Maryland" }
@STRING{icfp11 = icfp # ", Tokyo, Japan" }
@STRING{icfp12 = icfp # ", Copenhagen, Denmark" }
@STRING{icfp13 = icfp # ", Boston, Massachusetts" }
@STRING{icfp14 = icfp # ", Gothenburg, Sweden" }
@STRING{icfp15 = icfp # ", Vancouver, British Columbia, Canada" }
@STRING{icfp16 = icfp # ", Nara, Japan" }
@STRING{icfp17 = icfp # ", Oxford, United Kingdom" }
@STRING{icfp18 = icfp # ", St. Louis, Missouri" }
% ----
@STRING{oopsla = "{ACM} {S}ymposium on {O}bject {O}riented {P}rogramming:
{S}ystems, {L}anguages, and {A}pplications ({OOPSLA})" }
@STRING{oopsla86 = oopsla # ", Portland, Oregon" }
@STRING{oopsla89 = oopsla }
@STRING{oopsla98 = oopsla # ", Vancouver, British Columbia" }
@STRING{oopsla08 = oopsla # ", Nashville, Tennessee" }
% ----
@STRING{lics = "IEEE Symposium on Logic in Computer Science (LICS)" }
@STRING{lics91 = lics # ", Amsterdam, The Netherlands" }
@STRING{lics92 = lics # ", Santa Cruz, California" }
@STRING{lics93 = lics # ", Montreal, Canada" }
@STRING{lics94 = lics # ", Paris, France" }
@STRING{lics95 = lics # ", San Diego, California" }
@STRING{lics96 = lics # ", New Brunswick, New Jersey" }
@STRING{lics97 = lics # ", Warsaw, Poland" }}
@STRING{lics98 = lics # ", Indianapolis, Indiana" }
@STRING{lics99 = lics # ", Trento, Italy" }
@STRING{lics00 = lics # ", Santa Barbara, California" }
@STRING{lics01 = lics # ", Boston, Massachusetts" }
@STRING{lics02 = lics # ", Copenhagen, Denmark" }
@STRING{lics03 = lics # ", Ottawa, Canada" }
@STRING{lics04 = lics # ", Turku, Finland" }
@STRING{lics05 = lics # ", Chicago, Illinois" }
@STRING{lics06 = lics # ", Seattle, Washington" }
@STRING{lics07 = lics # ", Wroclaw, Poland" }
@STRING{lics08 = lics # ", Pittsburgh, Pennsylvania" }
@STRING{lics09 = lics # ", Los Angeles, California" }
@STRING{lics10 = lics # ", Edinburgh, Scotland" }
@STRING{lics11 = lics # ", Toronto, Canada" }
@STRING{lics12 = lics # ", Dubrovnik, Croatia" }
@STRING{lics13 = lics # ", New Orleans, Louisiana" }
@STRING{lics14 = lics # ", Vienna, Austria" }
@STRING{lics17 = lics # ", Reykjavik, Iceland" }
% ----
@STRING{pldi = "{ACM SIGPLAN Conference on Programming Language Design
and Implementation (PLDI)}" }
@STRING{pldi88 = pldi # ", {A}tlanta, {G}eorgia" }
@STRING{pldi89 = pldi # ", Portland, Oregon" }
@STRING{pldi90 = pldi # ", White Plains, New York" }
@STRING{pldi91 = pldi # ", Toronto, Ontario" }
@STRING{pldi92 = pldi # ", San Francisco, California" }
@STRING{pldi93 = pldi # ", Albuquerque, New Mexico" }
@STRING{pldi94 = pldi # ", Orlando, Florida" }
@STRING{pldi95 = pldi # ", La Jolla, California" }
@STRING{pldi96 = pldi # ", Philadephia, Pennsylvania" }
@STRING{pldi97 = pldi # ", Las Vegas, Nevada" }
@STRING{pldi98 = pldi # ", {M}ontreal, {C}anada" }
@STRING{pldi99 = pldi # ", {A}tlanta, {G}eorgia" }
@STRING{pldi00 = pldi # ", Vancouver, British Columbia, Canada" }
@STRING{pldi01 = pldi # ", Snowbird, Utah" }
@STRING{pldi02 = pldi # ", Berlin, Germany" }
@STRING{pldi03 = pldi # ", San Diego, California" }
@STRING{pldi04 = pldi # ", Washington, DC" }
@STRING{pldi05 = pldi # ", Chicago, Illinois" }
@STRING{pldi06 = pldi # ", Ottawa, Canada" }
@STRING{pldi07 = pldi # ", San Diego, California" }
@STRING{pldi08 = pldi # ", Tucson, Arizona" }
@STRING{pldi09 = pldi # ", Dublin, Ireland" }
@STRING{pldi10 = pldi # ", Toronto, Canada" }
@STRING{pldi11 = pldi # ", San Jose, California" }
@STRING{pldi12 = pldi # ", Beijing, China" }
@STRING{pldi13 = pldi # ", Seattle, Washington" }
@STRING{pldi14 = pldi # ", Edinburgh, Scotland" }
% ----
@STRING{lfp = "ACM Symposium on Lisp and Functional Programming (LFP)" }
@STRING{lfp84 = lfp # ", Austin, Texas" }
@STRING{lfp88 = lfp # ", Snowbird, Utah" }
@STRING{lfp90 = lfp }
@STRING{lfp92 = lfp }
% ----
@STRING{fpca = "ACM Symposium on Functional Programming Languages and
Computer Architecture (FPCA)" }
@STRING{fpca89 = fpca }
@STRING{fpca93 = fpca }
% ----
@STRING{sosp=" {ACM} {S}ymposium on {O}perating {S}ystems {P}rinciples ({SOSP})"}
% ----
@STRING{fool = "Workshop on Foundations of Object-Oriented Languages
(FOOL), informal proceedings" }
@STRING{tlca = "Typed Lambda Calculi and Applications (TLCA)" }
@STRING{tlca93 = tlca # ", Utrecht, The Netherlands" }
@STRING{tlca95 = tlca # ", Edinburgh, UK" }
@STRING{tlca97 = tlca # ", Nancy, France" }
@STRING{tlca99 = tlca # ", L'Aquila, Italy" }
@STRING{tlca01 = tlca # ", Krakow, Poland" }
@STRING{tlca03 = tlca # ", Valencia, Spain" }
@STRING{tlca05 = tlca # ", Nara, Japan" }
@STRING{tlca07 = tlca # ", Paris, France" }
@STRING{tlca09 = tlca # ", Brasilia, Brazil" }
@STRING{tlca11 = tlca # ", Novi Sad, Serbia" }
@STRING{tlca13 = tlca # ", Eindhoven, The Netherlands" }
@string{fscd = "Formal Structures for Computation and Deduction"}
@string{fscd18 = fscd # ", Oxford England"}
@string{cav = "Conference on Computer Aided Verification (CAV)"}
@string{ccs = "ACM Conference on Computer and Communication Security (CCS)"}
@string{oakland = "{IEEE} Symposium on Security and Privacy"}
@string{dls = "Dynamic Languages Symposium (DLS)"}
@STRING{esop = "European Symposium on Programming (ESOP)" }
@STRING{esop92 = esop # ", Rennes, France" }
@STRING{ecoop = "{E}uropean {C}onference on {O}bject-{O}riented
{P}rogramming ({ECOOP})" }
@STRING{ecoop97 = ecoop }
@STRING{ecoop02 = ecoop # ", Malaga, Spain" }
@STRING{flops = "International Symposium on Functional and Logic Programming (FLOPS)" }
@STRING{flops02 = flops # ", Aizu, Japan" }
@string{icalp = "International Colloquium on Automata, Languages and Programming (ICALP)"}
@string{plpv = "Programming Languages meets Program Verification (PLPV)"}
@STRING{post = "Principles of Security and Trust (POST)" }
@string{ppdp = "ACM Conference on Principles and Practice of Declarative Programming (PPDP)"}
@string{scheme = "Scheme and Functional Programming Workshop (Scheme)"}
@string{stop = "Workshop on Script-to-Program Evolution (STOP)"}
@string{tldi = "ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI)"}
@STRING{tacs = "Theoretical Aspects of Computer Software (TACS)" }
@STRING{tacs01 = tacs # ", Sendai, Japan" }
@string{tfp = "Trends in Functional Programming (TFP)"}
@STRING{webdb = {International Workshop on the Web and Databases
(WebDB)} }
@STRING{langsec = "Language-theoretic Security IEEE Security and Privacy Workshop (LangSec)"}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@INPROCEEDINGS{Nakano2000,
author={Nakano, H.},
booktitle={Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332)},
title={A modality for recursion},
year={2000},
volume={},
number={},
pages={255-266},
doi={10.1109/LICS.2000.855774}}
@article{Mannaa2020TickingCA,
title={Ticking clocks as dependent right adjoints: Denotational semantics for clocked type theory},
author={Bassel Mannaa and Rasmus Ejlers M{\o}gelberg and Niccol{\`o} Veltri},
journal={Log. Methods Comput. Sci.},
year={2020},
volume={16}
}
@inproceedings{mogelberg-paviotti2016,
author = {M\o{}gelberg, Rasmus Ejlers and Paviotti, Marco},
title = {Denotational Semantics of Recursive Types in Synthetic Guarded Domain Theory},
year = {2016},
isbn = {9781450343916},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2933575.2934516},
doi = {10.1145/2933575.2934516},
abstract = {Guarded recursion is a form of recursion where recursive calls are guarded by delay modalities. Previous work has shown how guarded recursion is useful for reasoning operationally about programming languages with advanced features including general references, recursive types, countable non-determinism and concurrency.Guarded recursion also offers a way of adding recursion to type theory while maintaining logical consistency. In previous work we initiated a programme of denotational semantics in type theory using guarded recursion, by constructing a computationally adequate model of the language PCF (simply typed lambda calculus with fixed points). This model was intensional in that it could distinguish between computations computing the same result using a different number of fixed point unfoldings.In this work we show how also programming languages with recursive types can be given denotational semantics in type theory with guarded recursion. More precisely, we give a computationally adequate denotational semantics to the language FPC (simply typed lambda calculus extended with recursive types), modelling recursive types using guarded recursive types. The model is intensional in the same way as was the case in previous work, but we show how to recover extensionality using a logical relation.All constructions and reasoning in this paper, including proofs of theorems such as soundness and adequacy, are by (informal) reasoning in type theory, often using guarded recursion.},
booktitle = {Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science},
pages = {317-326},
numpages = {10},
keywords = {Synthetic Domain Theory, Denotational Semantics, Guarded Recursion, Type Theory, Recursive Types},
location = {New York, NY, USA},
series = {LICS '16}
}
@inproceedings{veltri-vezzosi2020,
author = {Veltri, Niccol\`{o} and Vezzosi, Andrea},
title = {Formalizing $\pi$-Calculus in Guarded Cubical Agda},
year = {2020},
isbn = {9781450370974},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3372885.3373814},
doi = {10.1145/3372885.3373814},
abstract = {Dependent type theories with guarded recursion have shown themselves suitable for the development of denotational semantics of programming languages. In particular Ticked Cubical Type Theory (TCTT) has been used to show that for guarded labelled transition systems (GLTS) interpretation into the denotational semantics maps bisimilar processes to equal values. In fact the two notions are proved equivalent, allowing one to reason about equality in place of bisimilarity. We extend that result to the π-calculus, picking early congruence as the syntactic notion of equivalence between processes, showing that denotational models based on guarded recursive types can handle the dynamic creation of channels that goes beyond the scope of GLTSs. Hence we present a fully abstract denotational model for the early π-calculus, formalized as an extended example for Guarded Cubical Agda: a novel implementation of Ticked Cubical Type Theory based on Cubical Agda.},
booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs},
pages = {270-283},
numpages = {14},
keywords = {pi-calculus, ticked cubical type theory, denotational semantics, guarded recursion},
location = {New Orleans, LA, USA},
series = {CPP 2020}
}
@INPROCEEDINGS{birkedal-mogelberg-schwinghammer-stovring2011,
author={Birkedal, Lars and Mogelberg, Rasmus Ejlers and Schwinghammer, Jan and Stovring, Kristian},
booktitle={2011 IEEE 26th Annual Symposium on Logic in Computer Science},
title={First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees},
year={2011},
volume={},
number={},
pages={55-64},
doi={10.1109/LICS.2011.16}}
@INPROCEEDINGS{bahr-grathwohl-bugge-mogelberg2017,
author={Bahr, Patrick and Grathwohl, Hans Bugge and Møgelberg, Rasmus Ejlers},
booktitle={2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
title={The clocks are ticking: No more delays!},
year={2017},
volume={},
number={},
pages={1-12},
doi={10.1109/LICS.2017.8005097}}
@inproceedings{atkey-mcbride2013,
author = {Atkey, Robert and McBride, Conor},
title = {Productive Coprogramming with Guarded Recursion},
year = {2013},
isbn = {9781450323260},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2500365.2500597},
doi = {10.1145/2500365.2500597},
abstract = {Total functional programming offers the beguiling vision that, just by virtue of the compiler accepting a program, we are guaranteed that it will always terminate. In the case of programs that are not intended to terminate, e.g., servers, we are guaranteed that programs will always be productive. Productivity means that, even if a program generates an infinite amount of data, each piece will be generated in finite time. The theoretical underpinning for productive programming with infinite output is provided by the category theoretic notion of final coalgebras. Hence, we speak of coprogramming with non-well-founded codata, as a dual to programming with well-founded data like finite lists and trees.Systems that offer facilities for productive coprogramming, such as the proof assistants Coq and Agda, currently do so through syntactic guardedness checkers. Syntactic guardedness checkers ensure that all self-recursive calls are guarded by a use of a constructor. Such a check ensures productivity. Unfortunately, these syntactic checks are not compositional, and severely complicate coprogramming.Guarded recursion, originally due to Nakano, is tantalising as a basis for a flexible and compositional type-based approach to coprogramming. However, as we show, by itself, guarded recursion is not suitable for coprogramming due to the fact that there is no way to make finite observations on pieces of infinite data. In this paper, we introduce the concept of clock variables that index Nakano's guarded recursion. Clock variables allow us to "close over" the generation of infinite data, and to make finite observations, something that is not possible with guarded recursion alone.},
booktitle = {Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming},
pages = {197-208},
numpages = {12},
keywords = {total functional programming, guarded recursion, coalgebras, corecursion},
location = {Boston, Massachusetts, USA},
series = {ICFP '13}
}
@article{10.1145/2544174.2500597,
author = {Atkey, Robert and McBride, Conor},
title = {Productive Coprogramming with Guarded Recursion},
year = {2013},
issue_date = {September 2013},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {48},
number = {9},
issn = {0362-1340},
url = {https://doi.org/10.1145/2544174.2500597},
doi = {10.1145/2544174.2500597},
abstract = {Total functional programming offers the beguiling vision that, just by virtue of the compiler accepting a program, we are guaranteed that it will always terminate. In the case of programs that are not intended to terminate, e.g., servers, we are guaranteed that programs will always be productive. Productivity means that, even if a program generates an infinite amount of data, each piece will be generated in finite time. The theoretical underpinning for productive programming with infinite output is provided by the category theoretic notion of final coalgebras. Hence, we speak of coprogramming with non-well-founded codata, as a dual to programming with well-founded data like finite lists and trees.Systems that offer facilities for productive coprogramming, such as the proof assistants Coq and Agda, currently do so through syntactic guardedness checkers. Syntactic guardedness checkers ensure that all self-recursive calls are guarded by a use of a constructor. Such a check ensures productivity. Unfortunately, these syntactic checks are not compositional, and severely complicate coprogramming.Guarded recursion, originally due to Nakano, is tantalising as a basis for a flexible and compositional type-based approach to coprogramming. However, as we show, by itself, guarded recursion is not suitable for coprogramming due to the fact that there is no way to make finite observations on pieces of infinite data. In this paper, we introduce the concept of clock variables that index Nakano's guarded recursion. Clock variables allow us to "close over" the generation of infinite data, and to make finite observations, something that is not possible with guarded recursion alone.},
journal = {SIGPLAN Not.},
month = {sep},
pages = {197-208},
numpages = {12},
keywords = {guarded recursion, coalgebras, total functional programming, corecursion}
}
@inproceedings{kristensen-mogelberg-vezzosi2022,
author = {Baunsgaard Kristensen, Magnus and Mogelberg, Rasmus Ejlers and Vezzosi, Andrea},
title = {Greatest HITs: Higher Inductive Types in Coinductive Definitions via Induction under Clocks},
year = {2022},
isbn = {9781450393515},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/3531130.3533359},
doi = {10.1145/3531130.3533359},
abstract = {We present Clocked Cubical Type Theory, the first type theory combining multi-clocked guarded recursion with the features of Cubical Type Theory. Guarded recursion is an abstract form of step-indexing, which can be used for construction of advanced programming language models. In its multi-clocked version, it can also be used for coinductive programming and reasoning, encoding productivity in types. Combining this with Higher Inductive Types (HITs) the encoding extends to coinductive types that are traditionally hard to represent in type theory, such as the type of finitely branching labelled transition systems. Among our technical contributions is a new principle of induction under clocks, providing computational content to one of the main axioms required for encoding coinductive types. This principle is verified using a denotational semantics in a presheaf model.},
booktitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science},
articleno = {42},
numpages = {13},
location = {Haifa, Israel},
series = {LICS '22}
}
@article{mogelberg-veltri2019,
author = {M\o{}gelberg, Rasmus Ejlers and Veltri, Niccol\`{o}},
title = {Bisimulation as Path Type for Guarded Recursive Types},
year = {2019},
issue_date = {January 2019},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {3},
number = {POPL},
url = {https://doi.org/10.1145/3290317},
doi = {10.1145/3290317},
abstract = {In type theory, coinductive types are used to represent processes, and are thus crucial for the formal verification of non-terminating reactive programs in proof assistants based on type theory, such as Coq and Agda. Currently, programming and reasoning about coinductive types is difficult for two reasons: The need for recursive definitions to be productive, and the lack of coincidence of the built-in identity types and the important notion of bisimilarity. Guarded recursion in the sense of Nakano has recently been suggested as a possible approach to dealing with the problem of productivity, allowing this to be encoded in types. Indeed, coinductive types can be encoded using a combination of guarded recursion and universal quantification over clocks. This paper studies the notion of bisimilarity for guarded recursive types in Ticked Cubical Type Theory, an extension of Cubical Type Theory with guarded recursion. We prove that, for any functor, an abstract, category theoretic notion of bisimilarity for the final guarded coalgebra is equivalent (in the sense of homotopy type theory) to path equality (the primitive notion of equality in cubical type theory). As a worked example we study a guarded notion of labelled transition systems, and show that, as a special case of the general theorem, path equality coincides with an adaptation of the usual notion of bisimulation for processes. In particular, this implies that guarded recursion can be used to give simple equational reasoning proofs of bisimilarity. This work should be seen as a step towards obtaining bisimilarity as path equality for coinductive types using the encodings mentioned above.},
journal = {Proc. ACM Program. Lang.},
month = {jan},
articleno = {4},
numpages = {29},
keywords = {guarded recursion, labelled transition systems, bisimulation, homotopy type theory, coinductive types, Dependent types, cubical type theory, CCS}
}
@article{new-ahmed2018,
author = {New, Max S. and Ahmed, Amal},
title = {Graduality from Embedding-Projection Pairs},
year = {2018},
issue_date = {September 2018},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {2},
number = {ICFP},
url = {https://doi.org/10.1145/3236768},
doi = {10.1145/3236768},
abstract = {Gradually typed languages allow statically typed and dynamically typed code to interact while maintaining benefits of both styles. The key to reasoning about these mixed programs is Siek-Vitousek-Cimini-Boyland’s (dynamic) gradual guarantee, which says that giving components of a program more precise types only adds runtime type checking, and does not otherwise change behavior. In this paper, we give a semantic reformulation of the gradual guarantee called graduality. We change the name to promote the analogy that graduality is to gradual typing what parametricity is to polymorphism. Each gives a local-to-global, syntactic-to-semantic reasoning principle that is formulated in terms of a kind of observational approximation. Utilizing the analogy, we develop a novel logical relation for proving graduality. We show that embedding-projection pairs (ep pairs) are to graduality what relations are to parametricity. We argue that casts between two types where one is “more dynamic” (less precise) than the other necessarily form an ep pair, and we use this to cleanly prove the graduality cases for casts from the ep-pair property. To construct ep pairs, we give an analysis of the type dynamism relation—also known as type precision or na\"{\i}ve subtyping—that interprets the rules for type dynamism as compositional constructions on ep pairs, analogous to the coercion interpretation of subtyping.},
journal = {Proc. ACM Program. Lang.},
month = {jul},
articleno = {73},
numpages = {30},
keywords = {logical relations, gradual typing, observational error approximation, dynamic gradual guarantee}
}
@article{new-licata-ahmed2019,
author = {New, Max S. and Licata, Daniel R. and Ahmed, Amal},
title = {Gradual Type Theory},
year = {2019},
issue_date = {January 2019},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {3},
number = {POPL},
url = {https://doi.org/10.1145/3290328},
doi = {10.1145/3290328},
abstract = {Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. While existing gradual type soundness theorems for these languages aim to show that type-based reasoning is preserved when moving from the fully static setting to a gradual one, these theorems do not imply that correctness of type-based refactorings and optimizations is preserved. Establishing correctness of program transformations is technically difficult, because it requires reasoning about program equivalence, and is often neglected in the metatheory of gradual languages. In this paper, we propose an axiomatic account of program equivalence in a gradual cast calculus, which we formalize in a logic we call gradual type theory (GTT). Based on Levy’s call-by-push-value, GTT gives an axiomatic account of both call-by-value and call-by-name gradual languages. Based on our axiomatic account we prove many theorems that justify optimizations and refactorings in gradually typed languages. For example, uniqueness principles for gradual type connectives show that if the βη laws hold for a connective, then casts between that connective must be equivalent to the so-called “lazy” cast semantics. Contrapositively, this shows that “eager” cast semantics violates the extensionality of function types. As another example, we show that gradual upcasts are pure functions and, dually, gradual downcasts are strict functions. We show the consistency and applicability of our axiomatic theory by proving that a contract-based implementation using the lazy cast semantics gives a logical relations model of our type theory, where equivalence in GTT implies contextual equivalence of the programs. Since GTT also axiomatizes the dynamic gradual guarantee, our model also establishes this central theorem of gradual typing. The model is parametrized by the implementation of the dynamic types, and so gives a family of implementations that validate type-based optimization and the gradual guarantee.},
journal = {Proc. ACM Program. Lang.},
month = {jan},
articleno = {15},
numpages = {31},
keywords = {gradual typing, call-by-push-value, graduality}
}
@InProceedings{siek_et_al:LIPIcs:2015:5031,
author = {Jeremy G. Siek and Michael M. Vitousek and Matteo Cimini and John Tang Boyland},
title = {{Refined Criteria for Gradual Typing}},
booktitle = {1st Summit on Advances in Programming Languages (SNAPL 2015)},
pages = {274--293},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-939897-80-4},
ISSN = {1868-8969},
year = {2015},
volume = {32},
editor = {Thomas Ball and Rastislav Bodik and Shriram Krishnamurthi and Benjamin S. Lerner and Greg Morrisett},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2015/5031},
URN = {urn:nbn:de:0030-drops-50312},
doi = {10.4230/LIPIcs.SNAPL.2015.274},
annote = {Keywords: gradual typing, type systems, semantics, dynamic languages}
}
@inproceedings{garcia-clark-tanter2016,
author = {Garcia, Ronald and Clark, Alison M. and Tanter, \'{E}ric},
title = {Abstracting Gradual Typing},
year = {2016},
isbn = {9781450335492},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2837614.2837670},
doi = {10.1145/2837614.2837670},
abstract = {Language researchers and designers have extended a wide variety of type systems to support gradual typing, which enables languages to seamlessly combine dynamic and static checking. These efforts consistently demonstrate that designing a satisfactory gradual counterpart to a static type system is challenging, and this challenge only increases with the sophistication of the type system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs. In this paper, we propose a new formal foundation for gradual typing, drawing on principles from abstract interpretation to give gradual types a semantics in terms of pre-existing static types. Abstracting Gradual Typing (AGT for short) yields a formal account of consistency---one of the cornerstones of the gradual typing approach---that subsumes existing notions of consistency, which were developed through intuition and ad hoc reasoning. Given a syntax-directed static typing judgment, the AGT approach induces a corresponding gradual typing judgment. Then the type safety proof for the underlying static discipline induces a dynamic semantics for gradual programs defined over source-language typing derivations. The AGT approach does not resort to an externally justified cast calculus: instead, run-time checks naturally arise by deducing evidence for consistent judgments during proof reduction. To illustrate the approach, we develop a novel gradually-typed counterpart for a language with record subtyping. Gradual languages designed with the AGT approach satisfy by construction the refined criteria for gradual typing set forth by Siek and colleagues.},
booktitle = {Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {429-442},
numpages = {14},
keywords = {abstract interpretation, gradual typing, subtyping},
location = {St. Petersburg, FL, USA},
series = {POPL '16}
}
@article{10.1145/2914770.2837670,
author = {Garcia, Ronald and Clark, Alison M. and Tanter, \'{E}ric},
title = {Abstracting Gradual Typing},
year = {2016},
issue_date = {January 2016},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {51},
number = {1},
issn = {0362-1340},
url = {https://doi.org/10.1145/2914770.2837670},
doi = {10.1145/2914770.2837670},
abstract = {Language researchers and designers have extended a wide variety of type systems to support gradual typing, which enables languages to seamlessly combine dynamic and static checking. These efforts consistently demonstrate that designing a satisfactory gradual counterpart to a static type system is challenging, and this challenge only increases with the sophistication of the type system. Gradual type system designers need more formal tools to help them conceptualize, structure, and evaluate their designs. In this paper, we propose a new formal foundation for gradual typing, drawing on principles from abstract interpretation to give gradual types a semantics in terms of pre-existing static types. Abstracting Gradual Typing (AGT for short) yields a formal account of consistency---one of the cornerstones of the gradual typing approach---that subsumes existing notions of consistency, which were developed through intuition and ad hoc reasoning. Given a syntax-directed static typing judgment, the AGT approach induces a corresponding gradual typing judgment. Then the type safety proof for the underlying static discipline induces a dynamic semantics for gradual programs defined over source-language typing derivations. The AGT approach does not resort to an externally justified cast calculus: instead, run-time checks naturally arise by deducing evidence for consistent judgments during proof reduction. To illustrate the approach, we develop a novel gradually-typed counterpart for a language with record subtyping. Gradual languages designed with the AGT approach satisfy by construction the refined criteria for gradual typing set forth by Siek and colleagues.},
journal = {SIGPLAN Not.},
month = {jan},
pages = {429-442},
numpages = {14},
keywords = {subtyping, gradual typing, abstract interpretation}
}
@inproceedings{cimini-siek2016,
author = {Cimini, Matteo and Siek, Jeremy G.},
title = {The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems},
year = {2016},
isbn = {9781450335492},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/2837614.2837632},
doi = {10.1145/2837614.2837632},
abstract = {Many languages are beginning to integrate dynamic and static typing. Siek and Taha offered gradual typing as an approach to this integration that provides a coherent and full-span migration between the two disciplines. However, the literature lacks a general methodology for designing gradually typed languages. Our first contribution is to provide a methodology for deriving the gradual type system and the compilation to the cast calculus. Based on this methodology, we present the Gradualizer, an algorithm that generates a gradual type system from a well-formed type system and also generates a compiler to the cast calculus. Our algorithm handles a large class of type systems and generates systems that are correct with respect to the formal criteria of gradual typing. We also report on an implementation of the Gradualizer that takes a type system expressed in lambda-prolog and outputs its gradually typed version and a compiler to the cast calculus in lambda-prolog.},
booktitle = {Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {443-455},
numpages = {13},
keywords = {type systems, methodology, semantics, gradual typing},
location = {St. Petersburg, FL, USA},
series = {POPL '16}
}
@article{10.1145/2914770.2837632,
author = {Cimini, Matteo and Siek, Jeremy G.},
title = {The Gradualizer: A Methodology and Algorithm for Generating Gradual Type Systems},
year = {2016},
issue_date = {January 2016},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {51},
number = {1},
issn = {0362-1340},
url = {https://doi.org/10.1145/2914770.2837632},
doi = {10.1145/2914770.2837632},
abstract = {Many languages are beginning to integrate dynamic and static typing. Siek and Taha offered gradual typing as an approach to this integration that provides a coherent and full-span migration between the two disciplines. However, the literature lacks a general methodology for designing gradually typed languages. Our first contribution is to provide a methodology for deriving the gradual type system and the compilation to the cast calculus. Based on this methodology, we present the Gradualizer, an algorithm that generates a gradual type system from a well-formed type system and also generates a compiler to the cast calculus. Our algorithm handles a large class of type systems and generates systems that are correct with respect to the formal criteria of gradual typing. We also report on an implementation of the Gradualizer that takes a type system expressed in lambda-prolog and outputs its gradually typed version and a compiler to the cast calculus in lambda-prolog.},
journal = {SIGPLAN Not.},
month = {jan},
pages = {443-455},
numpages = {13},
keywords = {gradual typing, methodology, semantics, type systems}
}
@inproceedings{wadler-findler09,
author = "Philip Wadler and Robert Bruce Findler",
title = "Well-typed programs can't be blamed",
booktitle = esop,
year = 2009,
month = mar,
pages = "1--16",
location = "York, UK"
}
@inproceedings{tobin-hochstadt06,
author = "Sam Tobin-Hochstadt and Matthias Felleisen",
title = "Interlanguage Migration: From Scripts to Programs",
booktitle = dls,
month = oct,
pages = "964--974",
year = 2006,
}
@inproceedings{tobin-hochstadt08,
author = {Sam Tobin-Hochstadt and Matthias Felleisen},
title = {The Design and Implementation of Typed Scheme},
booktitle = popl08,
year = {2008}}
@inproceedings{siek-taha06,
author = "Jeremy G. Siek and Walid Taha",
title = "Gradual Typing for Functional Languages",
booktitle = scheme,
month = sep,
pages = "81--92",
year = 2006
}
@inproceedings{findler-felleisen02,
author = {Robert Bruce Findler and Matthias Felleisen},
title = {Contracts for higher-order functions},
booktitle = icfp,
year = {2002},
month = sep,
pages = {48--59}
}
@inproceedings{new-licata18,
author = {Max S. New and Daniel R. Licata},
title = {Call-by-name Gradual Type Theory},
booktitle = fscd18,
year = {2018},
doi = {10.4230/LIPIcs.FSCD.2018.24},
}
@phdthesis{levy01:phd,
author = "Levy, Paul Blain",
title = "Call-by-Push-Value",
type = "{Ph.~D.} Dissertation",
school = "Queen Mary, University of London",
department = "Department of Computer Science",
address = "London, UK",
month = mar,
year = "2001"}
@article{Capretta2005GeneralRV,
title={General recursion via coinductive types},
author={Venanzio Capretta},
journal={Log. Methods Comput. Sci.},
year={2005},
volume={1}
}
@article{CohenCoquandHuberMortberg2017,
title={Cubical type theory: A constructive interpretation of the univalence axiom},
author={Cyril Cohen and Thierry Coquand and Simon Huber and Anders M\"{o}rtberg},
journal={IFCoLog J. Log. Appl.},
year={2017}
}
@article{VezzosiMortbergAbel2019,
author = {Vezzosi, Andrea and M\"{o}rtberg, Anders and Abel, Andreas},
title = {Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types},
year = {2019},
issue_date = {August 2019},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {3},
number = {ICFP},
url = {https://doi.org/10.1145/3341691},
doi = {10.1145/3341691},
abstract = {Proof assistants based on dependent type theory provide expressive languages for both programming and proving within the same system. However, all of the major implementations lack powerful extensionality principles for reasoning about equality, such as function and propositional extensionality. These principles are typically added axiomatically which disrupts the constructive properties of these systems. Cubical type theory provides a solution by giving computational meaning to Homotopy Type Theory and Univalent Foundations, in particular to the univalence axiom and higher inductive types. This paper describes an extension of the dependently typed functional programming language Agda with cubical primitives, making it into a full-blown proof assistant with native support for univalence and a general schema of higher inductive types. These new primitives make function and propositional extensionality as well as quotient types directly definable with computational content. Additionally, thanks also to copatterns, bisimilarity is equivalent to equality for coinductive types. This extends Agda with support for a wide range of extensionality principles, without sacrificing type checking and constructivity.},
journal = {Proc. ACM Program. Lang.},
month = {jul},
articleno = {87},
numpages = {29},
keywords = {Univalence, Cubical Type Theory, Higher Inductive Types, Dependent Pattern Matching}
}
@article{new-jamner-ahmed19,
author = {New, Max S. and Jamner, Dustin and Ahmed, Amal},
title = {Graduality and Parametricity: Together Again for the First Time},
year = {2019},
issue_date = {January 2020},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {4},
number = {POPL},
url = {https://doi.org/10.1145/3371114},
doi = {10.1145/3371114},
abstract = {Parametric polymorphism and gradual typing have proven to be a difficult combination, with no language yet produced that satisfies the fundamental theorems of each: parametricity and graduality. Notably, Toro, Labrada, and Tanter (POPL 2019) conjecture that for any gradual extension of System F that uses dynamic type generation, graduality and parametricity are ``simply incompatible''. However, we argue that it is not graduality and parametricity that are incompatible per se, but instead that combining the syntax of System F with dynamic type generation as in previous work necessitates type-directed computation, which we show has been a common source of graduality and parametricity violations in previous work. We then show that by modifying the syntax of universal and existential types to make the type name generation explicit, we remove the need for type-directed computation, and get a language that satisfies both graduality and parametricity theorems. The language has a simple runtime semantics, which can be explained by translation to a statically typed language where the dynamic type is interpreted as a dynamically extensible sum type. Far from being in conflict, we show that the parametricity theorem follows as a direct corollary of a relational interpretation of the graduality property.},
journal = {Proc. ACM Program. Lang.},
month = {dec},
articleno = {46},
numpages = {32},
keywords = {graduality, gradual typing, polymorphism, parametricity, logical relation}
}
@article{lmcs:2265,
TITLE = {{General Recursion via Coinductive Types}},
AUTHOR = {Venanzio Capretta},
URL = {https://lmcs.episciences.org/2265},
DOI = {10.2168/LMCS-1(2:1)2005},
JOURNAL = {{Logical Methods in Computer Science}},
VOLUME = {{Volume 1, Issue 2}},
YEAR = {2005},
MONTH = Jul,
KEYWORDS = {Computer Science - Logic in Computer Science ; F.3.1},
}
@inproceedings{ma-reynolds,
author = {Ma, QingMing and Reynolds, John C.},
title = {Types, Abstractions, and Parametric Polymorphism, Part 2},
year = {1991},
isbn = {3540555110},
publisher = {Springer-Verlag},
address = {Berlin, Heidelberg},
booktitle = {Proceedings of the 7th International Conference on Mathematical Foundations of Programming Semantics},
pages = {1–40},
numpages = {40}
}
@phdthesis{dunphythesis,
author = {Dunphy, Brian Patrick},
advisor = {Reddy, Uday},
title = {Parametricity As a Notion of Uniformity in Reflexive Graphs},
year = {2002},
school = {University of Illinois at Urbana-Champaign},
address = {Champaign, IL, USA},
}
@article{reynoldsprogramme,
title = {Logical Relations and Parametricity – A Reynolds Programme for Category Theory and Programming Languages},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {303},
pages = {149-180},
year = {2014},
note = {Proceedings of the Workshop on Algebra, Coalgebra and Topology (WACT 2013)},
issn = {1571-0661},
doi = {https://doi.org/10.1016/j.entcs.2014.02.008},
url = {https://www.sciencedirect.com/science/article/pii/S1571066114000346},
author = {Claudio Hermida and Uday S. Reddy and Edmund P. Robinson},
keywords = {Universal algebra, Category Theory, Homomorphisms, Logical Relations, Natural Transformations, Parametric polymorphism, Relational Parametricity, Data abstraction, Information hiding, Definability, Reflexive Graphs, Fibrations, Relation lifting},
abstract = {In his seminal paper on “Types, Abstraction and Parametric Polymorphism,” John Reynolds called for homomorphisms to be generalized from functions to relations. He reasoned that such a generalization would allow type-based “abstraction” (representation independence, information hiding, naturality or parametricity) to be captured in a mathematical theory, while accounting for higher-order types. However, after 30 years of research, we do not yet know fully how to do such a generalization. In this article, we explain the problems in doing so, summarize the work carried out so far, and call for a renewed attempt at addressing the problem.}
}
@inproceedings{neis09,
author = {Georg Neis and Derek Dreyer and Andreas Rossberg},
title = {Non-Parametric Parametricity},
booktitle = icfp,
pages = "135--148",
year = {2009},
month = sep,
doi = {10.1145/1596550.1596572}
}
@inproceedings{ahmed06,
author = {Amal J. Ahmed},
editor = {Peter Sestoft},
title = {Step-Indexed Syntactic Logical Relations for Recursive and Quantified
Types},
booktitle = {Programming Languages and Systems, 15th European Symposium on Programming,
{ESOP} 2006, Held as Part of the Joint European Conferences on Theory
and Practice of Software, {ETAPS} 2006, Vienna, Austria, March 27-28,
2006, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {3924},
pages = {69--83},
publisher = {Springer},
year = {2006},
url = {https://doi.org/10.1007/11693024\_6},
doi = {10.1007/11693024\_6},
timestamp = {Tue, 05 Jul 2022 08:30:25 +0200},
}
@article{appelmcallester01,
author = {Appel, Andrew W. and McAllester, David},
title = {An indexed model of recursive types for foundational proof-carrying code},
year = {2001},
issue_date = {September 2001},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {23},
number = {5},
issn = {0164-0925},
url = {https://doi.org/10.1145/504709.504712},
doi = {10.1145/504709.504712},
journal = {ACM Trans. Program. Lang. Syst.},
month = {sep},
pages = {657–683},
numpages = {27}
}
@article{new-giovannini-licata-2022,
author = {Max S. New and
Eric Giovannini and
Daniel R. Licata},
title = {Gradual Typing for Effect Handlers},
journal = {Proc. {ACM} Program. Lang.},
volume = {7},
number = {{OOPSLA2}},
pages = {1758--1786},
year = {2023},
url = {https://doi.org/10.1145/3622860},
doi = {10.1145/3622860},
timestamp = {Sun, 10 Dec 2023 17:01:17 +0100},
biburl = {https://dblp.org/rec/journals/pacmpl/NewGL23.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{levy99,
author = {Paul Blain Levy},
editor = {Jean{-}Yves Girard},
title = {Call-by-Push-Value: {A} Subsuming Paradigm},
booktitle = {Typed Lambda Calculi and Applications, 4th International Conference,
TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {1581},
pages = {228--242},
publisher = {Springer},
year = {1999},
url = {https://doi.org/10.1007/3-540-48959-2\_17},
doi = {10.1007/3-540-48959-2\_17},
timestamp = {Tue, 14 May 2019 10:00:41 +0200},
}
@article{eec,
author = {Jeff Egger and
Rasmus Ejlers M{\o}gelberg and
Alex Simpson},
title = {The enriched effect calculus: syntax and semantics},
journal = {J. Log. Comput.},
volume = {24},
number = {3},
pages = {615--654},
year = {2014},
url = {https://doi.org/10.1093/logcom/exs025},
doi = {10.1093/LOGCOM/EXS025},
timestamp = {Wed, 17 May 2017 14:25:55 +0200},
biburl = {https://dblp.org/rec/journals/logcom/EggerMS14.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{cfm2016,
author = {Pierre{-}Louis Curien and
Marcelo P. Fiore and
Guillaume Munch{-}Maccagnoni},
editor = {Rastislav Bod{\'{\i}}k and
Rupak Majumdar},
title = {A theory of effects and resources: adjunction models and polarised
calculi},
booktitle = {Proceedings of the 43rd Annual {ACM} {SIGPLAN-SIGACT} Symposium on
Principles of Programming Languages, {POPL} 2016, St. Petersburg,
FL, USA, January 20 - 22, 2016},
pages = {44--56},
publisher = {{ACM}},
year = {2016},
url = {https://doi.org/10.1145/2837614.2837652},
doi = {10.1145/2837614.2837652},
timestamp = {Wed, 23 Jun 2021 15:34:31 +0200},
biburl = {https://dblp.org/rec/conf/popl/CurienFM16.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@phdthesis{Eremondi_2023, series={Electronic Theses and Dissertations (ETDs) 2008+}, title={On the design of a gradual dependently typed language for programming}, url={https://open.library.ubc.ca/collections/ubctheses/24/items/1.0428823}, DOI={http://dx.doi.org/10.14288/1.0428823}, school={University of British Columbia}, author={Eremondi, Joseph S.}, year={2023}, collection={Electronic Theses and Dissertations (ETDs) 2008+}}
@article{siek-chen2021,
author = {Jeremy G. Siek and
Tianyu Chen},
title = {Parameterized cast calculi and reusable meta-theory for gradually
typed lambda calculi},
journal = {J. Funct. Program.},
volume = {31},
pages = {e30},
year = {2021},
url = {https://doi.org/10.1017/S0956796821000241},
doi = {10.1017/S0956796821000241},
timestamp = {Fri, 21 Jan 2022 22:01:15 +0100},
biburl = {https://dblp.org/rec/journals/jfp/SiekC21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{FIORE_1997, title={An enrichment theorem for an axiomatisation of categories of domains and continuous functions}, volume={7}, DOI={10.1017/S0960129597002429}, number={5}, journal={Mathematical Structures in Computer Science}, author={FIORE, MARCELO P.}, year={1997}, pages={591–618}}
@article{GrodinNSH24,
author = {Harrison Grodin and
Yue Niu and
Jonathan Sterling and
Robert Harper},
title = {Decalf: {A} Directed, Effectful Cost-Aware Logical Framework},
journal = {Proc. {ACM} Program. Lang.},
volume = {8},
number = {{POPL}},
pages = {273--301},
year = {2024},
url = {https://doi.org/10.1145/3632852},
doi = {10.1145/3632852},
timestamp = {Thu, 25 Jan 2024 09:55:47 +0100},
biburl = {https://dblp.org/rec/journals/pacmpl/GrodinNSH24.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/corr/abs-2210-02169,
author = {Jonathan Sterling and
Daniel Gratzer and
Lars Birkedal},
title = {Denotational semantics of general store and polymorphism},
journal = {CoRR},
volume = {abs/2210.02169},
year = {2022},
url = {https://doi.org/10.48550/arXiv.2210.02169},
doi = {10.48550/ARXIV.2210.02169},
eprinttype = {arXiv},
eprint = {2210.02169},
timestamp = {Fri, 07 Oct 2022 15:24:59 +0200},
biburl = {https://dblp.org/rec/journals/corr/abs-2210-02169.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{action,
author = {G. Janelidze and G.M. Kelly},
title = { A Note on Actions of a Monoidal Category },
journal = {Theory and Applications of Categories},
volume = {9},
year = {2001},
number = {4},
pages = {61--91}
}