From 5d758e127d84000981441ded9a705f94bf6ec864 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Mon, 2 Dec 2024 14:03:28 -0500 Subject: [PATCH] papers: add tt-in-tt --- pnpm-lock.yaml | 16 ++++++++-------- src/.vitepress/readings.ts | 23 +++++++++++++++++++---- 2 files changed, 27 insertions(+), 12 deletions(-) diff --git a/pnpm-lock.yaml b/pnpm-lock.yaml index 1361d09..34b94fd 100644 --- a/pnpm-lock.yaml +++ b/pnpm-lock.yaml @@ -678,8 +678,8 @@ packages: engines: {node: ^6 || ^7 || ^8 || ^9 || ^10 || ^11 || ^12 || >=13.7} hasBin: true - caniuse-lite@1.0.30001684: - resolution: {integrity: sha512-G1LRwLIQjBQoyq0ZJGqGIJUXzJ8irpbjHLpVRXDvBEScFJ9b17sgK6vlx0GAJFE21okD7zXl08rRRUfq6HdoEQ==} + caniuse-lite@1.0.30001685: + resolution: {integrity: sha512-e/kJN1EMyHQzgcMEEgoo+YTCO1NGCmIYHk5Qk8jT6AazWemS5QFKJ5ShCJlH3GZrNIdZofcNCEwZqbMjjKzmnA==} ccount@2.0.1: resolution: {integrity: sha512-eyrF0jiFpY+3drT6383f1qhkbGsLSifNAjA61IUjZjmLCWjItY6LB9ft9YhoDgwfmclB2zhu51Lc7+95b8NRAg==} @@ -858,8 +858,8 @@ packages: resolution: {integrity: sha512-OCVPnIObs4N29kxTjzLfUryOkvZEq+pf8jTF0lg8E7uETuWHA+v7j3c/xJmiqpX450191LlmZfUKkXxkTry7nA==} engines: {node: ^10 || ^12 || >=14} - preact@10.25.0: - resolution: {integrity: sha512-6bYnzlLxXV3OSpUxLdaxBmE7PMOu0aR3pG6lryK/0jmvcDFPlcXGQAt5DpK3RITWiDrfYZRI0druyaK/S9kYLg==} + preact@10.25.1: + resolution: {integrity: sha512-frxeZV2vhQSohQwJ7FvlqC40ze89+8friponWUFeVEkaCfhC6Eu4V0iND5C9CXz8JLndV07QRDeXzH1+Anz5Og==} property-information@6.5.0: resolution: {integrity: sha512-PgTgs/BlvHxOu8QuEN7wi5A0OmXaBcHpmCSTehcs6Uuu9IkDIEo13Hy7n898RHfrQ49vKCoGeWZSaAK01nwVig==} @@ -1295,7 +1295,7 @@ snapshots: '@docsearch/js@3.8.0(@algolia/client-search@5.15.0)(search-insights@2.14.0)': dependencies: '@docsearch/react': 3.8.0(@algolia/client-search@5.15.0)(search-insights@2.14.0) - preact: 10.25.0 + preact: 10.25.1 transitivePeerDependencies: - '@algolia/client-search' - '@types/react' @@ -1691,12 +1691,12 @@ snapshots: browserslist@4.24.2: dependencies: - caniuse-lite: 1.0.30001684 + caniuse-lite: 1.0.30001685 electron-to-chromium: 1.5.67 node-releases: 2.0.18 update-browserslist-db: 1.1.1(browserslist@4.24.2) - caniuse-lite@1.0.30001684: {} + caniuse-lite@1.0.30001685: {} ccount@2.0.1: {} @@ -1876,7 +1876,7 @@ snapshots: picocolors: 1.1.1 source-map-js: 1.2.1 - preact@10.25.0: {} + preact@10.25.1: {} property-information@6.5.0: {} diff --git a/src/.vitepress/readings.ts b/src/.vitepress/readings.ts index 1803a88..270dd1b 100644 --- a/src/.vitepress/readings.ts +++ b/src/.vitepress/readings.ts @@ -78,7 +78,15 @@ const benjaminGregoire: Author = { } const brigittePientka: Author = { name: 'Brigitte Pientka', - link: 'https://www.cs.mcgill.ca/~bpientka/', + link: 'https://www.cs.mcgill.ca/~bpientka', +} +const altenkirch: Author = { + name: 'Thorsten Altenkirch', + link: 'https://people.cs.nott.ac.uk/psztxa', +} +const jcreed: Author = { + name: 'Jason Reed', + link: 'http://jcreed.org', } const universes: PublicationItem[] = [ @@ -152,6 +160,15 @@ const equality: PublicationItem[] = [ ['doi', '10.23638/LMCS-16(1:10)2020'] ], }, + { + title: 'Type Theory in Type Theory using Quotient Inductive Types', + authors: [altenkirch, akaposi], + venue: 'POPL 2016', + links: [ + ['doi', '10.1145/2837614.2837638'], + ['online', 'https://people.cs.nott.ac.uk/psztxa/publ/tt-in-tt.pdf'] + ] + }, { title: 'Contributions to Multimode and Presheaf Type Theory', authors: [{ @@ -331,9 +348,7 @@ const implicits: PublicationItem[] = [ }, { title: 'Higher-Order Constraint Simplification In Dependent Type Theory', - authors: [{ - name: 'Jason Reed', - }], + authors: [jcreed], venue: 'LFMTP 2009', links: [ ['doi', '10.1145/1577824.1577832'],