Skip header Section
Skip Bibliometrics Section
Basic simple type theoryNovember 1997
- Author:
- J. Roger Hindley
Abstract
No abstract available.
Cited By
Gavazzo F and Di Florio C (2023). Elements of Quantitative Rewriting, Proceedings of the ACM on Programming Languages, 7:POPL, (1832-1863), Online publication date: 9-Jan-2023.- MacQueen D, Harper R and Reppy J (2020). The history of Standard ML, Proceedings of the ACM on Programming Languages, 4:HOPL, (1-100), Online publication date: 14-Jun-2020.
- Ghilezan S, Ivetić J, Kašterović S, Ognjanović Z and Savić N Towards Probabilistic Reasoning in Type Theory - The Intersection Type Case Foundations of Information and Knowledge Systems, (122-139)
- Audrito G, Viroli M, Damiani F, Pianini D and Beal J (2019). A Higher-Order Calculus of Computational Fields, ACM Transactions on Computational Logic, 20:1, (1-55), Online publication date: 31-Jan-2019.
- Zeilberger N A theory of linear typings as flows on 3-valent graphs Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, (919-928)
- Lescanne P (2018). Quantitative Aspects of Linear and Affine Closed Lambda Terms, ACM Transactions on Computational Logic, 19:2, (1-18), Online publication date: 28-Jun-2018.
- Czajka ź and Kaliszyk C (2018). Hammer for Coq, Journal of Automated Reasoning, 61:1-4, (423-453), Online publication date: 1-Jun-2018.
- Bakel S (2018). Characterisation of Normalisation Properties for λμ using Strict Negated Intersection Types, ACM Transactions on Computational Logic, 19:1, (1-47), Online publication date: 15-Feb-2018.
- Dudenhefner A and Rehof J (2017). Intersection type calculi of bounded dimension, ACM SIGPLAN Notices, 52:1, (653-665), Online publication date: 11-May-2017.
- Dudenhefner A and Rehof J Intersection type calculi of bounded dimension Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, (653-665)
- Czajka Ł Improving automation in interactive theorem provers by efficient encoding of lambda-abstractions Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, (49-57)
- van Bakel S (2012). Completeness and Soundness Results for X with Intersection and Union Types, Fundamenta Informaticae, 121:1-4, (1-41), Online publication date: 1-Jan-2012.
- Baral C, Gonzalez M and Gottesman A The inverse lambda calculus algorithm for typed first order logic lambda calculus and its application to translating english to FOL Correct Reasoning, (40-56)
- Yoshinaka R and Kanazawa M Distributional learning of abstract categorial grammars Proceedings of the 6th international conference on Logical aspects of computational linguistics, (251-266)
- Bourreau P and Salvati S Game semantics and uniqueness of type inhabitance in the simply-typed λ-calculus Proceedings of the 10th international conference on Typed lambda calculi and applications, (61-75)
- Bakel S (2011). Strict intersection types for the Lambda Calculus, ACM Computing Surveys, 43:3, (1-49), Online publication date: 1-Apr-2011.
- Courbot A, Grimaud G and Vandewalle J (2010). Efficient off-board deployment and customization of virtual machine-based embedded systems, ACM Transactions on Embedded Computing Systems, 9:3, (1-53), Online publication date: 1-Feb-2010.
- Wright A (2010). Type theory comes of age, Communications of the ACM, 53:2, (16-17), Online publication date: 1-Feb-2010.
- Lienhardt M, Mezzina C, Schmitt A and Stefani J Typing Component-Based Communication Systems Proceedings of the Joint 11th IFIP WG 6.1 International Conference FMOODS '09 and 29th IFIP WG 6.1 International Conference FORTE '09 on Formal Techniques for Distributed Systems, (167-181)
- Erkök L and Matthews J Pragmatic equivalence and safety checking in Cryptol Proceedings of the 3rd workshop on Programming languages meets program verification, (73-82)
- Lienhardt M, Schmitt A and Stefani J Typing communicating component assemblages Proceedings of the 7th international conference on Generative programming and component engineering, (125-136)
- Kamareddine F, Nour K, Rahli V and Wells J A Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables Proceedings of the 5th international colloquium on Theoretical Aspects of Computing, (171-185)
- Comini M, Damiani F and Vrech S On Polymorphic Recursion, Type Systems, and Abstract Interpretation Proceedings of the 15th international symposium on Static Analysis, (144-158)
- Ventura D, Ayala-Rincón M and Kamareddine F Principal Typings for Explicit Substitutions Calculi Proceedings of the 4th conference on Computability in Europe: Logic and Theory of Algorithms, (567-578)
- Irwin R (2008). Review of "Derivation and Computation: Taking the Curry-Howard Correspondence Seriously by Harold Simmons," Cambridge University Press, 2000, ACM SIGACT News, 39:2, (42-44), Online publication date: 1-Jun-2008.
- Bono V, Venneri B and Bettini L (2008). A typed lambda calculus with intersection types, Theoretical Computer Science, 398:1-3, (95-113), Online publication date: 20-May-2008.
- Bunder M The inhabitation problem for intersection types Proceedings of the fourteenth symposium on Computing: the Australasian theory - Volume 77, (7-14)
- Coquand T (2007). The Completeness of Typing for Context-Semantics, Fundamenta Informaticae, 77:4, (293-301), Online publication date: 1-Dec-2007.
- Coquand T (2007). The Completeness of Typing for Context-Semantics, Fundamenta Informaticae, 77:4, (293-301), Online publication date: 1-Aug-2007.
- Lipton J and Nieva S Higher-order logic programming languages with constraints Proceedings of the 8th international conference on Typed lambda calculi and applications, (272-289)
- Abramsky S (2005). A structural approach to reversible computation, Theoretical Computer Science, 347:3, (441-464), Online publication date: 1-Dec-2005.
- Laird J Decidability in syntactic control of interference Proceedings of the 32nd international conference on Automata, Languages and Programming, (904-916)
- Damiani F Rank-2 intersection and polymorphic recursion Proceedings of the 7th international conference on Typed Lambda Calculi and Applications, (146-161)
- Coquand T Completeness theorems and π-calculus Proceedings of the 7th international conference on Typed Lambda Calculi and Applications, (1-9)
- Wells J and Yakobowski B Graph-based proof counting and enumeration with applications for program fragment synthesis Proceedings of the 14th international conference on Logic Based Program Synthesis and Transformation, (262-277)
- Damiani F Rank 2 intersection types for modules Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, (67-78)
- Taha W and Nielsen M (2003). Environment classifiers, ACM SIGPLAN Notices, 38:1, (26-37), Online publication date: 15-Jan-2003.
- Taha W and Nielsen M Environment classifiers Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (26-37)
- Andrews P Classical type theory Handbook of automated reasoning, (965-1007)
- van den Bussche J and Waller E Type inference in the polymorphic relational algebra Proceedings of the eighteenth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, (80-90)
Index Terms
- Basic simple type theory
Recommendations
Partial Gradual Dependent Type Theory
SPLASH 2023: Companion Proceedings of the 2023 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for HumanityGradual typing supports imprecise types in the type system, allowing incremental migration from untyped code to typed in the same language. Through the gradual typing approach, our ongoing work proposes a new theory based on the Martin-Löf type theory ...
Parametric quantifiers for dependent type theory
Polymorphic type systems such as System F enjoy the parametricity property: polymorphic functions cannot inspect their type argument and will therefore apply the same algorithm to any type they are instantiated on. This idea is formalized mathematically ...
Gradual type theory
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 ...