Normalisation by evaluation for type theory, in type theory

QR Code

Normalisation by evaluation for type theory, in type theory

We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction, and every constru...

Full description

Bibliographic Details
Main Authors:	Altenkirch, Thorsten, Kaposi, Ambrus
Format:	Article
Published:	Logical Methods in Computer Science e.V. 2017
Subjects:	normalisation by evaluation; dependent types; internal type theory; logical relations; Agda
Online Access:	https://eprints.nottingham.ac.uk/47642/

Similar Items

Normalisation by evaluation for dependent types
by: Altenkirch, Thorsten, et al.
Published: (2016)

Type theory in type theory using quotient inductive types
by: Altenkirch, Thorsten, et al.
Published: (2016)

Type theory in a type theory with quotient inductive types
by: Kaposi, Ambrus
Published: (2017)

Towards a cubical type theory without an interval
by: Altenkirch, Thorsten, et al.
Published: (2017)

Extending homotopy type theory with strict equality
by: Altenkirch, Thorsten, et al.
Published: (2016)

Quotient types in type theory
by: Li, Nuo
Published: (2015)

Types with extra structure: predicates, equations, composition
by: Hewer, Brandon
Published: (2024)

Notions of anonymous existence in Martin-Löf type theory
by: Kraus, Nicolai, et al.
Published: (2016)

Bootstrapping extensionality
by: Sestini, Filippo
Published: (2023)

Agent-Based Logics in Dependent Type Theory
by: Baston, Colm
Published: (2025)

Learning of interval and general type-2 fuzzy logic systems using simulated annealing: theory and practice
by: Almaraashia, M., et al.
Published: (2016)

Partiality, revisited: the partiality monad as a quotient inductive-inductive type
by: Altenkirch, Thorsten, et al.
Published: (2017)

Truncation levels in homotopy type theory
by: Kraus, Nicolai
Published: (2015)

Higher inductive types, inductive families, and inductive-inductive types
by: von Raumer, Jakob
Published: (2020)

Handling uncertainty: from type-1 to interval type-2 fuzzy sets and systems
by: Aladi, Jabran
Published: (2016)

Constructions with non-recursive higher inductive types
by: Kraus, Nicolai
Published: (2016)

A framework for relating, implementing and verifying argumentation models and their translations
by: van Gijzel, Bas
Published: (2016)

Effectiveness of a nurse-led diabetes self-management education on glycosylated hemoglobin among Iranian adults with type 2 diabetes
by: Azami, Golnaz
Published: (2019)

On Nie-Tan operator and type-reduction of interval type-2 fuzzy sets
by: Li, Jiawei, et al.
Published: (2018)

Effect of Diet, Insulin and Exercise on the Regulation of Carbohydrate Metabolism in Health and Type 1 Diabetes
by: Chokkalingam, Kamalakkannan
Published: (2007)

Interval type-2 fuzzy modelling and stochastic search for real-world inventory management
by: Miller, Simon, et al.
Published: (2012)

Free higher groups in homotopy type theory
by: Kraus, Nicolai, et al.
Published: (2018)

Influence of vegetation and soil types on the wheatbelt termite, Drepanotermes tamminensis (Hill), in the Western Australian wheatbelt
by: Park, H., et al.
Published: (1994)

A novel framework for the implementation and evaluation of type-1 and interval type-2 ANFIS
by: Chen, Chao
Published: (2018)

A Study on Relationship Between Decision-making Behaviour and Myers-Briggs Type Indicator
by: Chen, Jelico
Published: (2007)

Type-2 fuzzy linear systems
by: Najariyan, Marzieh, et al.
Published: (2017)

Interval type-2 A-intuitionistic fuzzy logic for regression problems
by: Eyoh, Imo, et al.
Published: (2017)

Interval type-2 intuitionistic fuzzy logic systems - a comparative evaluation
by: Eyoh, Imo, et al.
Published: (2018)

The role of C-type lectin receptors in the recognition of Pseudiminas aeruginosa
by: Alshahrani, Mohammad
Published: (2018)

Study of bandgap property of a bilayer membrane-type metamaterial applied on a thin plate
by: GAO, Cong, et al.
Published: (2020)

Analysis of g s-transferase, protien tyrosine phosphatase 1B, nuclear factor kappa-B1 and leptin receptor genetic polymorphisms as risk factors for Malaysian type 2 diabetes mellitus subjects
by: Etemad, Ali
Published: (2013)

Prediction of bandgaps in membrane-type metamaterial attached to a thin plate
by: Gao, Cong, et al.
Published: (2019)

Improving security requirements adequacy: an interval type 2 fuzzy logic security assessment system
by: Hibshi, Hanan, et al.
Published: (2016)

Type-2 fuzzy elliptic membership functions for modeling uncertainty
by: Kayacan, Erdal, et al.
Published: (2018)

Univalent higher categories via complete semi-segal types
by: Capriotti, Paolo, et al.
Published: (2018)

Analysis of gastrointestinal microbiota in relation to obesity and type 2 diabetes among adults
by: Kaliyappan, Roseni
Published: (2015)

Interval type-2 intuitionistic fuzzy logic systems: a comparative evaluation
by: Eyoh, Imo, et al.
Published: (2018)

Factors associated with glycaemic control among diabetes mellitus type 2 patients attending health clinics in Tampin district Negeri Sembilan, Malaysia
by: Wan Hamdzan, Wan Farzana Fasya
Published: (2016)

Elliptic membership functions and the modeling uncertainty in type-2 fuzzy logic systems as applied to time series prediction
by: Kayacan, Erdal, et al.
Published: (2017)

Exploring the micro-politics of normalisation: Narratives of pleasure, self-control and desire in a sample of young Australian ‘party drug’ users
by: Pennay, Amy, et al.
Published: (2010)