Type System Implementation (researchr/bibliography/publications)

researchr

You are not signed in
Sign in
Sign up

Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewritingMichael Färber. CPP 2022: 225-238 [doi] [classification] 6 months ago

RefinedC: automating the foundational verification of C code with refined ownership typesMichael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg 0001. PLDI 2021: 158-174 [doi] [classification] 6 months ago

RefinedRust: A Type System for High-Assurance Verification of Rust ProgramsLennard Gäher, Michael Sammler, Ralf Jung 0002, Robbert Krebbers, Derek Dreyer. PACMPL, 8(PLDI):1115-1139, 2024. [doi] [classification] 6 months ago

ELPI: Fast, Embeddable, \lambda Prolog InterpreterCvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi. lpar 2015: 460-468 [doi] [classification] 7 months ago

Autosubst 2: reasoning with multi-sorted de Bruijn terms and vector substitutionsKathrin Stark, Steven Schäfer, Jonas Kaiser. CPP 2019: 166-180 [doi] [classification] 7 months ago

Type-Directed Elaboration of Quasiquotations: A High-Level Syntax for Low-Level ReflectionDavid Raymond Christiansen. IFL 2014: 1 [doi] [classification] 7 months ago

Elaborating Inductive DefinitionsPierre-Evariste Dagand, Conor McBride. 2012. [classification] 7 months ago

Autosubst: Reasoning with de Bruijn Terms and Parallel SubstitutionsSteven Schäfer, Tobias Tebbi, Gert Smolka. itp 2015: 359-374 [doi] [classification] 7 months ago

TinkerType: a language for playing with formal systemsMichael Y. Levin, Benjamin C. Pierce. JFP, 13(2):295-316, 2003. [doi] [classification] 7 months ago

alpha-Prolog: A Logic Programming Language with Names, Binding and a-EquivalenceJames Cheney, Christian Urban. ICLP 2004: 269-283 [doi] [classification] 7 months ago

Unification in Many-Sorted Algebras as a Device for Incremental Semantic AnalysisGregor Snelting, Wolfgang Henhapl. POPL 1986: 229-235 [classification] 7 months ago

Executable Specification of Static SemanticsThierry Despeyroux. sdt 1984: 215-233 [classification] 7 months ago

The PSG System: From Formal Language Definitions to Interactive Programming EnvironmentsRolf Bahlke, Gregor Snelting. TOPLAS, 8(4):547-576, 1986. [doi] [classification] 7 months ago

A tutorial implementation of dynamic pattern unification: A dependently typed programming language implementation pearlAdam Gundry, Conor McBride. 2012. [classification] 7 months ago

Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specificationsArjen Rouvoet, Hendrik van Antwerpen, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser. PACMPL, 4(OOPSLA), 2020. [doi] [classification] 10 months ago

Implementing type theory in higher order constraint logic programmingFerruccio Guidi, Claudio Sacerdoti Coen, Enrico Tassi. mscs, 29(8):1125-1150, 2019. [doi] [classification] 10 months ago

Dependent Types in Practical ProgrammingHongwei Xi, Frank Pfenning. POPL 1999: 214-227 [doi] [classification] 2 years ago

A dependently typed calculus with pattern matching and erasure inferenceMatus Tejiscak. PACMPL, 4(ICFP), 2020. [doi] [classification] 3 years ago

A quick look at impredicativityAlejandro Serrano 0001, Jurriaan Hage, Simon Peyton Jones, Dimitrios Vytiniotis. PACMPL, 4(ICFP), 2020. [doi] [classification] 3 years ago

Elaboration with first-class implicit function typesAndrás Kovács. PACMPL, 4(ICFP), 2020. [doi] [classification] 3 years ago

A metaprogramming framework for formal verificationGabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, Leonardo de Moura. PACMPL, 1(ICFP), 2017. [doi] [classification] 3 years ago

The Lean 4 Theorem Prover and Programming LanguageLeonardo de Moura, Sebastian Ullrich. cade 2021: 625-635 [doi] [classification] 3 years ago

Beyond Notations: Hygienic Macro Expansion for Theorem Proving LanguagesSebastian Ullrich, Leonardo de Moura. cade 2020: 167-182 [doi] [classification] 3 years ago

The Constructive EngineGérard Huet. In R. Narasimhan, editor, A Perspective in Theoretical Computer Science - Commemorative Volume for Gift Siromoney. Volume 16 of World Scientific Series in Computer Science, pages 38-69, World Scientific, 1989. [doi] [classification] 3 years ago

Type checking through unificationFrancesco Mazzoli, Andreas Abel. 2016. [classification] 3 years ago

Local type inferenceBenjamin C. Pierce, David N. Turner. TOPLAS, 22(1):1-44, 2000. [doi] [classification] 3 years ago

An Algorithm for Type-Checking Dependent TypesThierry Coquand. SCP, 26(1-3):167-177, 1996. [classification] 3 years ago

Programming up to CongruenceVilhelm Sjöberg, Stephanie Weirich. POPL 2015: 369-382 [doi] [classification] 3 years ago

The theory of LEGORobert Pollack. PhD thesis, 1995. [doi] [classification] 3 years ago

Checking Algorithms for Pure Type SystemsL. S. van Benthem Jutting, James McKinna, Robert Pollack. TYPES 1994: 19-61 [classification] 3 years ago

An insider's look at LF type reconstruction: everything you (n)ever wanted to knowBrigitte Pientka. JFP, 23(1):1-37, 2013. [doi] [classification] 3 years ago

Universe Polymorphism in CoqMatthieu Sozeau, Nicolas Tabareau. itp 2014: 499-514 [doi] [classification] 4 years ago

A simple type-theoretic language: Mini-TTThierry Coquand, Yoshiki Kinoshita, Bengt Nordström, Makoto Takeyama. From Semantics to Computer Science; Essays in Honour of Gilles Kahn, :139-164, 2009. [classification] 4 years ago

Dependent ML An approach to practical programming with dependent typesHongwei Xi. JFP, 17(2):215-286, 2007. [doi] [classification] 4 years ago

Design and Implementation of the Andromeda Proof AssistantAndrej Bauer, Gaëtan Gilbert, Philipp G. Haselwarter, Matija Pretnar, Christopher A. Stone. TYPES 2018: [doi] [classification] 4 years ago

Bidirectional Elaboration of Dependently Typed ProgramsFrancisco Ferreira, Brigitte Pientka. ppdp 2014: 161-174 [doi] [classification] 4 years ago

Implementing a modal dependent type theoryDaniel Gratzer, Jonathan Sterling, Lars Birkedal. PACMPL, 3(ICFP), 2019. [doi] [classification] 4 years ago

Type inference, Haskell and dependent typesAdam Michael Gundry. PhD thesis, University of Strathclyde, Glasgow, UK, 2013. [doi] [classification] 4 years ago

The Little TyperFriedman, Daniel P, Christiansen, David Thrane. MIT Press, 2018. [classification] 4 years ago

A Tutorial Implementation of a Dependently Typed Lambda CalculusAndres Löh, Conor McBride, Wouter Swierstra. FUIN, 102(2):177-207, 2010. [doi] [classification] 4 years ago

Aspects of the Implementation of Type TheoryRobert W. Harper. PhD thesis, Cornell University, 1985. [classification] 4 years ago

A New Implementation of AutomathFreek Wiedijk. JAR, 29(3-4):365-387, 2002. [classification] 4 years ago

A compiled implementation of strong reductionBenjamin Grégoire, Xavier Leroy. ICFP 2002: 235-246 [doi] [classification] 4 years ago

Elf: A Language for Logic Definition and Verified MetaprogrammingFrank Pfenning. lics 1989: 313-322 [classification] 4 years ago

Functional pearl: I am not a number-I am a free variableConor McBride, James McKinna. haskell 2004: 1-9 [doi] [classification] 4 years ago

Idris 2: Quantitative Type Theory in ActionEdwin Brady. 2021. [classification] 4 years ago

Typechecking in the lambda-Pi-Calculus Modulo : Theory and Practice. (Vérification de typage pour le lambda-Pi-Calcul Modulo : théorie et pratique)Ronan Saillard. PhD thesis, Mines ParisTech, France, 2015. [doi] [classification] 4 years ago

Efficient rewriting using decision treesHondet, Gabriel. Master's thesis, ENAC ; Univesit{\'e} Toulouse III- Paul Sabatier, Aug 2019. [classification] 4 years ago

The New Rewriting Engine of Dedukti (System Description)Gabriel Hondet, Frédéric Blanqui. fscd 2020: [doi] [classification] 4 years ago

Small, Fast, Concurrent Proof Checking for the lambda-Pi Calculus Modulo RewritingMichael Färber. 2021. [classification] 4 years ago

Dependent type systems as macrosStephen Chang, Michael Ballantyne, Milo Turner, William J. Bowman. PACMPL, 4(POPL), 2020. [doi] [classification] 4 years ago

Growing a proof assistantBowman, William J. Higher-Order Programming with Effects, 65, 2016. [classification] 4 years ago

Implementation Techniques for Inductive Types in PlasticPaul Callaghan, Zhaohui Luo. TYPES 2000: 94-113 [doi] [classification] 4 years ago

GADTs meet their match: pattern-matching warnings that account for GADTs, guards, and lazinessGeorgios Karachalias, Tom Schrijvers, Dimitrios Vytiniotis, Simon L. Peyton Jones. ICFP 2015: 424-436 [doi] [classification] 4 years ago

A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof IrrelevanceAndreas Abel, Thierry Coquand, Miguel Pagano. tlca 2009: 5-19 [doi] [classification] 4 years ago

Mode and Termination Checking for Higher-Order Logic ProgramsEkkehard Rohwedder, Frank Pfenning. ESOP 1996: 296-310 [classification] 4 years ago

Optimizing Higher-Order Pattern UnificationBrigitte Pientka, Frank Pfenning. cade 2003: 473-487 [doi] [classification] 4 years ago

Algorithms for Equality and Unification in the Presence of Notational DefinitionsFrank Pfenning, Carsten Schürmann. ENTCS, 17:1-13, 1998. [doi] [classification] 4 years ago

An algorithm for testing conversion in type theoryCoquand, Thierry. Logical frameworks, 1:255-279, 1991. [classification] 4 years ago

A Coverage Checking Algorithm for LFCarsten Schürmann, Frank Pfenning. tphol 2003: 120-135 [doi] [classification] 4 years ago

Unnesting of CopatternsAnton Setzer, Andreas Abel, Brigitte Pientka, David Thibodeau. RTA 2014: 31-45 [doi] [classification] 4 years ago

An Existential Crisis Resolved: Type inference for first-class existential types Richard A. Eisenberg, Guillaume Duboc, Stephanie Weirich, Daniel Lee. 2021. [classification] 4 years ago

A role for dependent types in HaskellStephanie Weirich, Pritam Choudhury, Antoine Voizard, Richard A. Eisenberg. PACMPL, 3(ICFP), 2019. [doi] [classification] 4 years ago

User Interaction with the Matita Proof AssistantAndrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli. JAR, 39(2):109-139, 2007. [doi] [classification] 4 years ago

Crafting a Proof AssistantAndrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi, Stefano Zacchiroli. TYPES 2007: 18-32 [doi] [classification] 4 years ago

A compact kernel for the calculus of inductive constructionsA. Asperti, W. Ricciotti, Coen Sacerdoti, E. Tassi. , 2009. [doi] [classification] 4 years ago

Hints in UnificationAndrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi. tphol 2009: 84-98 [doi] [classification] 4 years ago

Nonuniform Coercions via Unification HintsSacerdoti Coen, Claudio, Tassi, Enrico. Electronic Proceedings in Theoretical Computer Science, 53, Mar 2011. [doi] [classification] 4 years ago

Practical dependent type checking using twin typesVíctor López Juan, Nils Anders Danielsson. ICFP 2020: 11-23 [doi] [classification] 4 years ago

MiniAgda: Integrating Sized and Dependent TypesAndreas Abel. itp 2012: 18-32 [doi] [classification] 4 years ago

Type checking in the presence of meta-variablesNorell, Ulf, Coquand, Catarina. , 2007. [classification] 4 years ago

Elaborator reflection: extending Idris in IdrisDavid Christiansen, Edwin Brady. ICFP 2016: 284-297 [doi] [classification] 4 years ago

Tabled Typeclass ResolutionDaniel Selsam, Sebastian Ullrich, Leonardo de Moura. CoRR, abs/2001.04301, 2020. [classification] 4 years ago

Equations reloaded: high-level dependently-typed functional programming and proving in CoqMatthieu Sozeau, Cyprien Mangin. PACMPL, 3(ICFP), 2019. [doi] [classification] 4 years ago

System Description: Twelf - A Meta-Logical Framework for Deductive SystemsFrank Pfenning, Carsten Schürmann. cade 1999: 202-206 [doi] [classification] 4 years ago

Inductive Families Need Not Store Their IndicesEdwin Brady, Conor McBride, James McKinna. TYPES 2004: 115-129 [doi] [classification] 4 years ago

Counting Immutable Beans: Reference Counting Optimized for Purely Functional ProgrammingSebastian Ullrich, Leonardo de Moura. CoRR, abs/1908.05647, 2019. [classification] 4 years ago

Elaboration in Dependent Type TheoryLeonardo Mendon{\c{c}}a de Moura, Jeremy Avigad, Soonho Kong, Cody Roux. CoRR, abs/1505.04324, 2015. [classification] 4 years ago

Congruence Closure in Intensional Type TheoryDaniel Selsam, Leonardo de Moura. cade 2016: 99-115 [doi] [classification] 4 years ago

A comprehensible guide to a new unifier for CIC including universe polymorphism and overloadingBeta Ziliani, Matthieu Sozeau. JFP, 27, 2017. [doi] [classification] 4 years ago

A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive ConstructionsAndrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi. Log. Methods Comput. Sci., 8(1), 2012. [doi] [classification] 4 years ago

The Lean Theorem Prover (System Description)Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, Jakob von Raumer. cade 2015: 378-388 [doi] [classification] 4 years ago

Towards a practical programming language based on dependent type theoryUlf Norell. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 G\"{o}teborg, Sweden, September 2007. [classification] 4 years ago

Idris, a general-purpose dependently typed programming language: Design and implementationEdwin Brady. JFP, 23(5):552-593, 2013. [doi] [classification] 4 years ago

Practical implementation of a dependently typed functional programming languageEdwin Brady. PhD thesis, Durham University, UK, 2005. [doi] [classification] 4 years ago

Elaborating dependent (co)pattern matching: No pattern left behindJesper Cockx, Andreas Abel. JFP, 30, 2020. [doi] [classification] 4 years ago

Type Theory Unchained: Extending Agda with User-Defined Rewrite RulesJesper Cockx. TYPES 2020: [doi] [classification] 4 years ago

OutsideIn(X) Modular type inference with local assumptionsDimitrios Vytiniotis, Simon L. Peyton Jones, Tom Schrijvers, Martin Sulzmann. J. Funct. Program., 21(4-5):333-412, 2011. [classification] 4 years ago

Epigram reloaded: a standalone typechecker for ETTJames Chapman, Thorsten Altenkirch, Conor McBride. sfp 2007: 79-94 [classification] 4 years ago

runs on WebDSL