Andreas Abel - researchr profile publications

researchr

You are not signed in
Sign in
Sign up

Publications with a 'Andreas Abel' as author, editor, or advisor:

Leibniz equality is isomorphic to Martin-Löf identity, parametricallyAndreas Abel 0001, Jesper Cockx, Dominique Devriese, Amin Timany, Philip Wadler. JFP, 30, 2020. [doi]
Type-based termination: a polymorphic lambda-calculus with sized higher-order typesAndreas Abel 0001. PhD thesis, Ludwig Maximilians University Munich, 2007.
On Model-Theoretic Strong Normalization for Truth-Table Natural DeductionAndreas Abel 0001. TYPES 2021: [doi]
Cubical Agda: A dependently typed programming language with univalence and higher inductive typesAndrea Vezzosi, Anders Mörtberg, Andreas Abel 0001. JFP, 31, 2021. [doi]
A Categorical Perspective on Pattern Unification (Extended Abstract)Andrea Vezzosi, Andreas Abel 0001. UNIF 2014: 69-73 [doi]
Primitive Recursion for Rank-2 Inductive TypesAndreas Abel 0001, Ralph Matthes. fics 2003: 1-3 [doi]
Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional EqualityAndreas Abel 0001, Thierry Coquand. lmcs, 16(2), 2020. [doi]
Proceedings of the 7th Workshop on Programming languages meets program verification, PLPV 2013, Rome, Italy, January 22, 2013Matthew Might, David Van Horn, Andreas Abel 0001, Tim Sheard, editors, ACM, 2013. [doi]
Implementing a Normalizer Using Sized Heterogeneous TypesAndreas Abel 0001. mpc 2006: [doi]
Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, LFMTP@LICS 2008, Pittsburgh, PA, USA, June 23, 2008Andreas Abel 0001, Christian Urban, editors, Volume 228 of Electronic Notes in Theoretical Computer Science, Elsevier, 2009. [doi]
23rd International Conference on Types for Proofs and Programs, TYPES 2017, May 29-June 1, 2017, Budapest, HungaryAndreas Abel 0001, Fredrik Nordvall Forsberg, Ambrus Kaposi, editors, Volume 104 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. [doi]
A Graded Modal Dependent Type Theory with a Universe and Erasure, FormalizedAndreas Abel 0001, Nils Anders Danielsson, Oskar Eriksson. PACMPL, 7(ICFP):920-954, August 2023. [doi]
Wellfounded recursion with copatterns: a unified approach to termination and productivityAndreas Abel 0001, Brigitte Pientka. ICFP 2013: 185-196 [doi]
Well-Founded Recursion over Contextual ObjectsBrigitte Pientka, Andreas Abel 0001. tlca 2015: 273-287 [doi]
Development and Verification of Complex Hybrid Systems Using Synthesizable MonitorsAndreas Abel, Allon Adir, Torsten Blochwitz, Lev Greenberg, Tamer Salman. hvc 2013: 182-198 [doi]
A Predicative Strong Normalisation Proof for a lambda-Calculus with Interleaving Inductive TypesAndreas Abel, Thorsten Altenkirch. TYPES 2000: 21-40 [doi]
Polarised subtyping for sized typesAndreas Abel. mscs, 18(5):797-822, 2008. [doi]
A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof IrrelevanceAndreas Abel, Thierry Coquand, Miguel Pagano. tlca 2009: 5-19 [doi]
Towards Normalization by Evaluation for the ::::betaeta::::-Calculus of ConstructionsAndreas Abel. FLOPS 2010: 224-239 [doi]
Untyped Algorithmic Equality for Martin-Löf s Logical Framework with Surjective PairsAndreas Abel, Thierry Coquand. tlca 2005: 23-38 [doi]
A unified view of modalities in type systemsAndreas Abel, Jean-Philippe Bernardy. PACMPL, 4(ICFP), 2020. [doi]
Syntactic Metatheory of Higher-Order SubtypingAndreas Abel, Dulma Rodriguez. csl 2008: 446-460 [doi]
A Partial Type Checking Algorithm for Type: TypeAndreas Abel, Thorsten Altenkirch. ENTCS, 229(5):3-17, 2011. [doi]
Verifying haskell programs using constructive type theoryAndreas Abel, Marcin Benke, Ana Bove, John Hughes, Ulf Norell. haskell 2005: 62-73 [doi]
Programming and Reasoning with Infinite Structures Using Copatterns and Sized TypesAndreas Abel. se 2014: 148-150 [doi]
A predicative analysis of structural recursionAndreas Abel, Thorsten Altenkirch. JFP, 12(1):1-41, 2002.
Fixed Points of Type Constructors and Primitive RecursionAndreas Abel, Ralph Matthes. csl 2004: 190-204 [doi]
Compositional Coinduction with Sized TypesAndreas Abel. cmcs 2016: 5-10 [doi]
Weak beta-theta-Normalization and Normalization by Evaluation for System FAndreas Abel. lpar 2008: 497-511 [doi]
Mixed Inductive/Coinductive Types and Strong NormalizationAndreas Abel. aplas 2007: 286-301 [doi]
On the Algebraic Foundation of Proof Assistants for Intuitionistic Type TheoryAndreas Abel, Thierry Coquand, Peter Dybjer. FLOPS 2008: 3-13 [doi]
Connecting a Logical Framework to a First-Order Logic ProverAndreas Abel, Thierry Coquand, Ulf Norell. frocos 2005: 285-301 [doi]
Untyped Algorithmic Equality for Martin-Löf s Logical Framework with Surjective PairsAndreas Abel, Thierry Coquand. FUIN, 77(4):345-395, 2007. [doi]
Typed Applicative Structures and Normalization by Evaluation for System F:::::::omega:::::::Andreas Abel. csl 2009: 40-54 [doi]
An analysis method for the performance comparison of communication systemsAndreas Abel, Marco Götz, Wolfgang Schwarz. icecsys 1998: 107-110 [doi]
Termination checking with typesAndreas Abel. ita, 38(4):277-319, 2004. [doi]
(Co-)Iteration for Higher-Order Nested DatatypesAndreas Abel, Ralph Matthes. TYPES 2003: 1-20 [doi]
Generalized Iteration and Coiteration for Higher-Order Nested DatatypesAndreas Abel, Ralph Matthes, Tarmo Uustalu. fossacs 2003: 54-69 [doi]
Verifying a Semantic beta-eta-Conversion Test for Martin-Löf Type TheoryAndreas Abel, Thierry Coquand, Peter Dybjer. mpc 2008: 29-56 [doi]
Higher-Order Dynamic Pattern Unification for Dependent Types and RecordsAndreas Abel, Brigitte Pientka. tlca 2011: 10-26 [doi]
Specification and Verification of a Formal System for Structurally Recursive FunctionsAndreas Abel. TYPES 2000: 1-20 [doi]
Termination and Productivity Checking with Continuous TypesAndreas Abel. tlca 2003: 1-15 [doi]
Type-based termination of generic programsAndreas Abel. SCP, 74(8):550-567, 2009. [doi]
A Third-Order Representation of the lambda-mu-CalculusAndreas Abel. TCS, 58(1):97-114, 2001. [doi]
Type checking through unificationFrancesco Mazzoli, Andreas Abel. 2016.
Private Währungen im Internet - Fachkonzept und EinsatzpotenzialeAndreas Abel, Claus Rautenstrauch. wirtschaftsinformatik 2003: 325-344
Semi-Continuous Sized Types and TerminationAndreas Abel. lmcs, 4(2), 2008. [doi]
Implementing a normalizer using sized heterogeneous typesAndreas Abel. JFP, 19(3-4):287-310, 2009. [doi]
A Formalized Proof of Strong Normalization for Guarded Recursive TypesAndreas Abel, Andrea Vezzosi. aplas 2014: 140-158 [doi]
Betrachtungen zur Schaffung oder Abbildung von Realitäten beispielhaft anhand eines E-Commerce-ProjektesAndreas Abel, Frank Wolff. gi 2001: 770-775
PrefaceAndreas Abel, Christian Urban. ENTCS, 228:1, 2009. [doi]
Polarized Subtyping for Sized TypesAndreas Abel. csr 2006: 381-392 [doi]
Irrelevance in Type Theory with a Heterogeneous Equality JudgementAndreas Abel. fossacs 2011: 57-71 [doi]
Normalization for the Simply-Typed Lambda-Calculus in TwelfAndreas Abel. ENTCS, 199:3-16, 2008. [doi]
Semi-continuous Sized Types and TerminationAndreas Abel. csl 2006: 72-88 [doi]
Strong Normalization and Equi-(Co)Inductive TypesAndreas Abel. tlca 2007: 8-22 [doi]
Iteration and coiteration schemes for higher-order and nested datatypesAndreas Abel, Ralph Matthes, Tarmo Uustalu. TCS, 333(1-2):3-66, 2005. [doi]
Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality JudgementsAndreas Abel, Thierry Coquand, Peter Dybjer. lics 2007: 3-12 [doi]
Normalization by Evaluation for Martin-Löf Type Theory with One UniverseAndreas Abel, Klaus Aehlig, Peter Dybjer. ENTCS, 173:17-39, 2007. [doi]
Towards Generic Programming with Sized TypesAndreas Abel. mpc 2006: 10-28 [doi]
Modeling bimodal electromigration failure distributionsA. H. Fischer, A. Abel, M. Lepper, A. E. Zitzelsberger, A. von Glasow. mr, 41(3):445-453, 2001. [doi]

runs on WebDSL