{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:05:56Z","timestamp":1763467556664},"reference-count":0,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2003,3,20]],"date-time":"2003-03-20T00:00:00Z","timestamp":1048118400000},"content-version":"unspecified","delay-in-days":19,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2003,3]]},"abstract":"<jats:p>TinkerType is a pragmatic framework for compact and modular description of formal systems \n(type systems, operational semantics, logics, etc.). A family of related systems is broken down \ninto a set of <jats:italic>clauses<\/jats:italic> \u2013 individual inference rules \u2013 and a set of <jats:italic>features<\/jats:italic> controlling the inclusion \nof clauses in particular systems. Simple static checks are used to help maintain consistency \nof the generated systems. We present TinkerType and its implementation and describe \nits application to two substantial repositories of typed lambda-calculi. The first repository \ncovers a broad range of typing features, including subtyping, polymorphism, type operators \nand kinding, computational effects, and dependent types. It describes both declarative and \nalgorithmic aspects of the systems, and can be used with our tool, the <jats:italic>TinkerType Assembler<\/jats:italic>, to \ngenerate calculi either in the form of typeset collections of inference rules or as executable ML \ntypecheckers. The second repository addresses a smaller collection of systems, and provides \nmodularized <jats:italic>proofs<\/jats:italic> of basic safety properties.<\/jats:p>","DOI":"10.1017\/s0956796802004550","type":"journal-article","created":{"date-parts":[[2003,3,27]],"date-time":"2003-03-27T15:04:19Z","timestamp":1048777459000},"page":"295-316","source":"Crossref","is-referenced-by-count":23,"title":["TinkerType: a language for playing with formal systems"],"prefix":"10.1017","volume":"13","author":[{"given":"MICHAEL Y.","family":"LEVIN","sequence":"first","affiliation":[]},{"given":"BENJAMIN C.","family":"PIERCE","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2003,3,20]]},"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796802004550","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,30]],"date-time":"2019-03-30T19:03:41Z","timestamp":1553972621000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796802004550\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,3]]},"references-count":0,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,3]]}},"alternative-id":["S0956796802004550"],"URL":"https:\/\/doi.org\/10.1017\/s0956796802004550","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,3]]}}}