开源软件名称(OpenSource Name):dpndnt/library
开源软件地址(OpenSource Url):https://github.com/dpndnt/library
开源编程语言(OpenSource Language):
TeX
100.0%
开源软件介绍(OpenSource Introduction):dpndnt/library
Research library of the ##dependent IRC channel.
A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
A
- A. Abel (2012) “Agda: Equality”
- A. Abel, S. Adelsberger, A. Setzer (2017) “Interactive programming in Agda: Objects and graphical user interfaces”
- A. Abel, J. Chapman (2014) “Normalization by evaluation in the delay monad: A case study for coinduction via copatterns and sized types”
- A. Abel, B. Pientka (2010) “Explicit substitutions for contextual type theory”
- S. Abramsky, A. Jung (1994) “Domain theory”
- P. Aczel (1977) “The type theoretic interpretation of constructive set theory”
- P. Aczel (1982) “The type theoretic interpretation of constructive set theory: Choice principles”
- G. Allais (2017) “Typing with leftovers: A mechanization of intuitionistic linear logic”
- N. Alechina, M. Mendler, V. de Paiva, E. Ritter (2001) “Categorical and Kripke semantics for constructive S4 modal logic”
- J. Alt, S. Artemov (2001) “Reflective λ-calculus”
- N. Amin, T. Rompf (2018) “Collapsing towers of interpreters”
- A. Appel (2001) “Foundational proof-carrying code”
- J. Armstrong (2003) “Making reliable distributed systems in the presence of software errors”
- J. Armstrong (2007) “A history of Erlang”
- S. Artemov (1999) “On explicit reflection in theorem proving and formal verification”
- S. Artemov (2001) “Explicit provability and constructive semantics”
- S. Artemov, E. Barzilay, R. Constable, A. Nogin (2001) “Reflection and propositions-as-types”
- S. Artemov, L. Beklemishev (2005) “Provability logic”
- S. Artemov, E. Bonelli (2007) “The intensional lambda calculus”
- S. Artemov, M. Fitting (2019) “Justification logic: Reasoning with reasons”
- S. Artemov, R. Iemhoff (2005) “The basic intuitionistic logic of proofs”
- R. Atkey, C. McBride (2013) “Productive coprogramming with guarded recursion”
- L. Augustsson (1985) “Compiling pattern matching”
- L. Augustsson (2006) “λ-calculus cooked four ways”
B
- R. Backhouse, P. Chisholm, G. Malcolm, E. Saaman (1989) “Do-it-yourself type theory”
- V. Balat, R. Di Cosmo, M. Fiore (2004) “Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums”
- D. Basin, S. Matthews, L. Viganò (1997) “Labelled propositional modal logics: Theory and practice”
- A. Bauer (2016) “On self-interpreters for Gödel’s System T”
- A. Bauer (2016) “On self-interpreters for System T and other typed λ-calculi”
- U. Berger, H. Schwichtenberg (1991) “An inverse of the evaluation functional for typed λ-calculus”
- J.-P. Bernardy, P. Jansson, R. Paterson (2010) “Parametricity and dependent types”
- G. Bierman, V. de Paiva (2000) “On an intuitionistic modal logic”
- E. Bishop (1973) “Schizophrenia in contemporary mathematics”
- E. Bishop (1975) “The crisis in contemporary mathematics”
- M. Boespflug, B. Pientka (2011) “Multi-level contextual type theory”
- E. Bonelli, F. Feller (2009) “The logic of proofs as a foundation for certifying mobile computation”
- M. Brown, J. Palsberg (2015) “Self-representation in Girard’s System U”
- M. Brown, J. Palsberg (2016) “Breaking through the normalization barrier: A self-interpreter for F-omega”
- M. Burrell, R. Cockett, B. Redmond (2009) “Pola: A language for PTIME programming”
- E. Burrows (2009) “A combinator processor”
C
- J. Carette, C.-H. Chen, V. Choudhury, A. Sabry (2018) “From reversible programs to univalent universes and back”
- J. Carette, O. Kiselyov, C.-C. Shan (2009) “Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages”
- J. Carette, A. Stump (2012) “Towards typing for small-step direct reflection”
- J. Chapman (2009) “Type checking and normalisation”
- J. Chapman, R. Kireev, C. Nester, P. Wadler (2019) “System F in Agda, for fun and profit”
- C.J. Cheney (1970) “A nonrecursive list compacting algorithm”
- A. Chlipala (2008) “Parametric higher-order abstract syntax for mechanized semantics”
- D.R. Christiansen (2013) “Bidirectional typing rules: A tutorial”
- T.J.W. Clarke, P.J.S. Gladstone, C.D. MacLean, A.C. Norman (1980) “SKIM: The S, K, I reduction machine”
- L. Convent, S. Lindley, C. McBride, C. McLaughlin (2020) “Doo bee doo bee doo”
- C. Coquand (2002) “A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions”
- T. Coquand (2004) “About Brouwer’s fan theorem”
- T. Coquand, P. Dybjer (1994) “Inductive definitions and type theory: An introduction (Preliminary version)”
- T. Coquand, P. Dybjer (1997) “Intuitionistic model constructions and normalization proofs”
D
- L. Damas, R. Milner (1982) “Principal type-schemes for functional programs”
- N. Danielsson (2012) “Operational semantics using the partiality monad”
- R. David, B. Guillaume (2001) “A λ-calculus with explicit weakening and explicit substitution”
- O. Danvy, M. Rhiger, K. Rose (2001) “Normalization by evaluation with typed abstract syntax”
- R. Davies (1996) “A temporal-logic approach to binding-time analysis”
- R. Davies, F. Pfenning (1996) “A modal analysis of staged computation”
- R. Davies, F. Pfenning (2001) “A modal analysis of staged computation”
- B. Delaware, B. Oliveira, T. Schrijvers (2013) “Meta-theory à la carte”
- J. Despeyroux, F. Pfenning, C. Schürmann (1997) “Primitive recursion for higher-order abstract syntax”
- D. Devriese, F. Piessens (2013) “Typed syntactic meta-programming”
- L. Diehl, D. Firsov, A. Stump (2018) “Generic zero-cost reuse for dependent types”
- L. Diehl (2017) “Fully generic programming over closed universes of inductive-recursive types”
- J. Dunfield, N. Krishnaswami (2019) “Bidirectional typing”
- P. Dybjer (1994) “Inductive families”
- P. Dybjer, A. Filinski (2002) “Normalization and partial evaluation”
- R. Dyckhoff (2015) “Some remarks on proof-theoretic semantics”
- R. Dyckhoff, L. Pinto (1997) “Proof search in constructive logics”
E
F
G
H
I
J
K
L
M
N
O
P
Q
R
S
T
U
V
W
X
Y
Z
|
请发表评论