{"entities":{"Q7361834":{"pageid":31521041,"ns":120,"title":"Item:Q7361834","lastrevid":105369851,"modified":"2026-10-07T13:38:39Z","type":"item","id":"Q7361834","labels":{"en":{"language":"en","value":"An Algebra for Higher-Order Terms"}},"descriptions":{"en":{"language":"en","value":"AFP entry Higher_Order_Terms"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2491ac87c68365caecdcea75455de0a13c5b287a","datavalue":{"value":"https://isa-afp.org/entries/Higher_Order_Terms.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361834$19A6F4FC-9209-4441-A12F-747ECC85A162","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"250f083a2ef1e7a7df79afad0acdd22e5799ecf5","datavalue":{"value":{"time":"+2019-01-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361834$6B034D34-A2AB-4BBA-BF64-3A02098706D3","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"bf5d485796582ea615cfd5e7c0148e1add1641d3","datavalue":{"value":"Lars Hupel","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361834$E652134A-F227-478D-B303-5E4A3FE6EE48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"c50a956af192729c6b98a043282b4cb2c3b94f84","datavalue":{"value":"Yu Zhang","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361834$5A8128CD-5A6C-4F91-A8A5-8864A43A69F4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"37a1729939b8c79606f88918a894a5dcfa5b7f1c","datavalue":{"value":{"text":"An Algebra for Higher-Order Terms","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361834$03D1DEFC-ADD8-4EB7-9B67-1BD102ABC5F5","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"55e3412ba47ade4c5e263b2d516c1c371cb400ac","datavalue":{"value":"In this formalization, I introduce a higher-order term algebra, generalizing the notions of free variables, matching, and substitution. The need arose from the work on a verified compiler from Isabelle to CakeML . Terms can be thought of as consisting of a generic (free variables, constants, application) and a specific part. As example applications, this entry provides instantiations for de-Bruijn terms, terms with named variables, and Blanchette\u2019s \u03bb-free higher-order terms . Furthermore, I implement translation functions between de-Bruijn terms and named terms and prove their correctness.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361834$0AAC2ADA-D857-421A-8D11-98E9ADBC809C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b8ba7b68057757d42cfdcb945f7c0c92fd593a89","datavalue":{"value":{"entity-type":"item","numeric-id":1074342,"id":"Q1074342"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361834$C2E5E616-0B1F-4CE5-B8B2-1215363CF50B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"78757e9c4e37a9fa53a10705a27e9c8cff416b63","datavalue":{"value":{"entity-type":"item","numeric-id":2324018,"id":"Q2324018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361834$FEFE3330-5650-4F32-A8A9-D4D4B05C34EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4feea37c535bd22cbdd726fd39655db123c9a3f5","datavalue":{"value":{"entity-type":"item","numeric-id":928672,"id":"Q928672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361834$EAA07630-CE5B-4050-ABDC-F5A4B0D69136","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c3003d2433d321429fa556d5386f6d8a37a29de","datavalue":{"value":{"entity-type":"item","numeric-id":1202066,"id":"Q1202066"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361834$1C73ED21-DC6D-40F5-A735-35A15822C71A","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361834$A04FF94B-FE9E-4BC7-A90C-0BE5A592DB3D","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"da51d3ec386e981523e814b55f201f5691a30ca7","datavalue":{"value":{"entity-type":"item","numeric-id":7361531,"id":"Q7361531"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361834$3E8F27F5-9162-4A95-A546-22509FB23AFB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"cd0c9d6eaf2232ef6bd24acb440211c3c1735214","datavalue":{"value":{"entity-type":"item","numeric-id":7361192,"id":"Q7361192"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361834$3C44E787-BAB4-4A88-B740-5E47FFEDFB50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"e0b5465b6a0d9e05645cdb7168eee1aaf7eb2845","datavalue":{"value":{"entity-type":"item","numeric-id":7361518,"id":"Q7361518"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361834$02407F4A-240B-4E1D-B1B4-9029D2600108","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"bbbd01ab6fe9cda8df6fdce217eef2d86891f550","datavalue":{"value":{"entity-type":"item","numeric-id":7360795,"id":"Q7360795"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361834$D8CB6D4D-B764-451D-BC78-98651BF3CB8F","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361834$2E6018D9-1247-4825-BECA-3EFCFDB25C8C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"An Algebra for Higher-Order Terms","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/An_Algebra_for_Higher-Order_Terms"}}}}}